Submission Details

Back to Submissions List

Challenge: minFac

Submitted by: GasStationManager

Submitted at: 2024-11-24 12:48:24

Code:

def minFac(a:Nat) (h: a>1): Nat 

:=sorry

First Theorem Proof:

theorem minFac_isfac(a:Nat)(h: a>1): ( (minFac a h) ∣a) ∧(minFac a h>1)

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmp63o5e0k4/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmp63o5e0k4/target.olean
Finished imports
Finished replay
---
def
minFac
(a : ℕ) → a > 1 → ℕ
:= fun (a : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
minFac_isfac
∀ (a : ℕ) (h : a > 1), minFac a h ∣ a ∧ minFac a h > 1
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmp63o5e0k4/proof.olean
Finished imports
Finished replay
---
def
minFac
(a : ℕ) → a > 1 → ℕ
:= fun (a : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
minFac_isfac
∀ (a : ℕ) (h : a > 1), minFac a h ∣ a ∧ minFac a h > 1
#[sorryAx]

Second Theorem Proof:

theorem minFac_ismin(a:Nat)(h:a>1): Not (∃ y>1,( y ∣ a) ∧y<minFac a h)

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmp63o5e0k4/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmp63o5e0k4/target2.olean
Finished imports
Finished replay
---
def
minFac
(a : ℕ) → a > 1 → ℕ
:= fun (a : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
minFac_ismin
∀ (a : ℕ) (h : a > 1), ¬∃ y > 1, y ∣ a ∧ y < minFac a h
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmp63o5e0k4/proof2.olean
Finished imports
Finished replay
---
def
minFac
(a : ℕ) → a > 1 → ℕ
:= fun (a : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
minFac_ismin
∀ (a : ℕ) (h : a > 1), ¬∃ y > 1, y ∣ a ∧ y < minFac a h
#[sorryAx]