Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: Command Master

Submitted at: 2024-11-15 11:57:40

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

:= decide_eq_true_iff

Status: Incorrect

Feedback:

/tmp/tmpze7wi_ao/proof.lean:8:3: error: type mismatch
  decide_eq_true_iff
has type
  decide ?m.1091 = true ↔ ?m.1091 : Prop
but is expected to have type
  (isPrime a = true) = True ↔ Nat.Prime a : Prop