Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: GasStationManager

Submitted at: 2025-07-15 11:42:21

Code:

import Mathlib.Data.Nat.Prime.Defs

def isPrime(a: Nat): Bool

:= (a > 1) && (a.minFac == a)

-- solution by Grok 4

First Theorem Proof:

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

:= by
  unfold isPrime
  simp only [Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq]
  rw [Nat.prime_def_minFac]
  simp [Nat.succ_le_iff]

Status: Correct

Feedback:

------------------
Replaying /root/CodeProofTheArena/temp/tmp8mm_wt0h/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/tmp8mm_wt0h/proof.olean
Finished imports
Finished replay
---
theorem
temp.tmp8mm_wt0h.proof._auxLemma.1
∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {a b : α}, ((a == b) = true) = (a = b)
#[propext]
---
def
isPrime
ℕ → Bool
:= fun (a : Nat) => Bool.and (Decidable.decide (GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) (Nat.decLt (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) a)) (BEq.beq.{0} Nat (instBEqOfDecidableEq.{0} Nat instDecidableEqNat) (Nat.minFac a) a)
#[propext, Classical.choice, Quot.sound]
---
theorem
isPrime_correct
∀ (a : ℕ), (isPrime a = true) = True ↔ Nat.Prime a
#[propext, Classical.choice, Quot.sound]
---
theorem
temp.tmp8mm_wt0h.proof._auxLemma.2
∀ {m n : ℕ}, (m.succ ≤ n) = (m < n)
#[propext]
Finished with no errors.