Submission Details

Back to Submissions List

Challenge: minFac

Submitted by: GasStationManager

Submitted at: 2024-11-24 09:56:58

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:

Compilation error for /root/CodeProofTheArena/temp/tmperzv9gzl/target.lean:
/root/CodeProofTheArena/temp/tmperzv9gzl/target.lean:4:4: warning: declaration uses 'sorry'
/root/CodeProofTheArena/temp/tmperzv9gzl/target.lean:7:54: error: expected token

Second Theorem Proof:

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

:=sorry

Status: Incorrect