Submission Details

Back to Submissions List

Challenge: solveSquare

Submitted by: GasStationManager

Submitted at: 2024-11-24 12:50:24

Code:

def solveSquare(t:Nat): Nat

:=sorry

First Theorem Proof:

theorem solveSquare_isgeq(t:Nat): (solveSquare t)*(solveSquare t)>=t

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpmfa7h7jo/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpmfa7h7jo/target.olean
Finished imports
Finished replay
---
def
solveSquare
ℕ → ℕ
:= fun (t : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveSquare_isgeq
∀ (t : ℕ), solveSquare t * solveSquare t ≥ t
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpmfa7h7jo/proof.olean
Finished imports
Finished replay
---
def
solveSquare
ℕ → ℕ
:= fun (t : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveSquare_isgeq
∀ (t : ℕ), solveSquare t * solveSquare t ≥ t
#[sorryAx]

Second Theorem Proof:

theorem solveSquare_ismin(t:Nat): Not (∃ y< (solveSquare t), y*y>=t)

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpmfa7h7jo/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpmfa7h7jo/target2.olean
Finished imports
Finished replay
---
def
solveSquare
ℕ → ℕ
:= fun (t : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveSquare_ismin
∀ (t : ℕ), ¬∃ y < solveSquare t, y * y ≥ t
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpmfa7h7jo/proof2.olean
Finished imports
Finished replay
---
def
solveSquare
ℕ → ℕ
:= fun (t : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveSquare_ismin
∀ (t : ℕ), ¬∃ y < solveSquare t, y * y ≥ t
#[sorryAx]