Submission Details

Back to Submissions List

Challenge: isPrime

Submitted by: GasStationManager

Submitted at: 2024-11-24 22:14:52

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:

found a problem in /root/CodeProofTheArena/temp/tmpase55sf5/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpase55sf5/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/tmpase55sf5/proof.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]