Submission Details

Back to Submissions List

Challenge: solveProg

Submitted by: GasStationManager

Submitted at: 2024-11-24 11:23:39

Code:

def solveProg(t:Nat):Nat

:=sorry

First Theorem Proof:

theorem solveProg_isgeq(t:Nat): (solveProg t)*((solveProg t)+1) >= t*2

:=sorry

Status: Incorrect

Feedback:

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

Second Theorem Proof:

theorem solveProg_ismin(t:Nat): Not (∃ y< (solveProg t), y*(y+1)>=t*2)

:=sorry

Status: Incorrect

Feedback:

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