Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: Robin

Submitted at: 2025-03-28 19:13:25

Code:

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

:= Nat.Prime a

First Theorem Proof:

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

:= by simp [isPrime]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmphldcaajz/target.olean
Finished imports
Finished replay
---
def
isPrime
ℕ → Bool
:= fun (a : Nat) => sorryAx.{1} Bool Bool.false
#[sorryAx]
---
theorem
isPrime_correct
∀ (a : ℕ), (isPrime a = true) = True ↔ Nat.Prime a
#[sorryAx, propext]
------------------
Replaying /root/CodeProofTheArena/temp/tmphldcaajz/proof.olean
Finished imports
Finished replay
---
def
isPrime
ℕ → Bool
:= fun (a : Nat) => Decidable.decide (Nat.Prime a) (Nat.decidablePrime a)
#[propext, Classical.choice, Quot.sound]
---
theorem
isPrime_correct
∀ (a : ℕ), (isPrime a = true) = True ↔ Nat.Prime a
#[propext, Classical.choice, Quot.sound]
---
theorem
isPrime.eq_1
∀ (a : ℕ), isPrime a = decide (Nat.Prime a)
#[propext, Classical.choice, Quot.sound]
Finished with no errors.