Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: Command Master

Submitted at: 2024-11-15 12:01:25

Code:

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

:= decide (Nat.Prime a)

First Theorem Proof:

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

:= iff_true.to_iff.symm.trans (iff_iff_eq.trans decide_eq_true_iff)

Status: Incorrect

Feedback:

/tmp/tmpcvo3vqc0/proof.lean:8:3: error: unknown constant 'iff_true.to_iff.symm.trans'