Submission Details

Back to Submissions List

Challenge: modInv

Submitted by: GasStationManager

Submitted at: 2024-11-24 10:05:21

Code:

import Mathlib.Data.Prime.Defs

def modInv(a: Nat) (p:Nat)(hp:p.Prime): Option Nat

:=sorry

First Theorem Proof:

theorem modInv_correct(a:Nat) (p:Nat)(hp:p.Prime):
  (∃ x:Nat, (a*x)%p=1)->(a*(modInv a p hp).get!)%p=1

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpzhpnx47j/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpzhpnx47j/target.olean
Finished imports
Finished replay
---
theorem
modInv_correct
∀ (a p : ℕ) (hp : Nat.Prime p), (∃ x, a * x % p = 1) → a * (modInv a p hp).get! % p = 1
#[propext, sorryAx]
---
def
modInv
ℕ → (p : ℕ) → Nat.Prime p → Option ℕ
:= fun (a : Nat) (p : Nat) (hp : Nat.Prime p) => sorryAx.{1} (Option.{0} Nat) Bool.false
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpzhpnx47j/proof.olean
Finished imports
Finished replay
---
theorem
modInv_correct
∀ (a p : ℕ) (hp : Nat.Prime p), (∃ x, a * x % p = 1) → a * (modInv a p hp).get! % p = 1
#[propext, sorryAx]
---
def
modInv
ℕ → (p : ℕ) → Nat.Prime p → Option ℕ
:= fun (a : Nat) (p : Nat) (hp : Nat.Prime p) => sorryAx.{1} (Option.{0} Nat) Bool.false
#[propext, sorryAx]

Second Theorem Proof:

theorem modInv_none(a:Nat) (p:Nat)(hp:p.Prime): (Not (∃ x, (a*x)%p=1))-> modInv a p hp=none

:=sorry

Status: Incorrect