Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: GasStationManager

Submitted at: 2024-11-24 22:08:46

Code:

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

:=sorry

First Theorem Proof:

theorem isPrime_correct(a: Nat): (isPrime a)=True <-> Nat.Prime a

:=sorry

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmp32x0uz1h/target.lean:
/root/CodeProofTheArena/temp/tmp32x0uz1h/target.lean:2:4: warning: declaration uses 'sorry'
/root/CodeProofTheArena/temp/tmp32x0uz1h/target.lean:5:54: error: unknown constant 'Nat.Prime'