Submission Details

Back to Submissions List

Challenge: solveGeom

Submitted by: GasStationManager

Submitted at: 2024-11-24 11:29:34

Code:

def solveGeom(a t:Nat)(h:a>1):Nat

:=sorry

First Theorem Proof:

theorem solveGeom_isgeq(a t:Nat)(h:a>1): a^((solveGeom a t h)+1)-1 >=t*(a-1)

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmp117v7r7f/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmp117v7r7f/target.olean
Finished imports
Finished replay
---
def
solveGeom
(a : ℕ) → ℕ → a > 1 → ℕ
:= fun (a : Nat) (t : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveGeom_isgeq
∀ (a t : ℕ) (h : a > 1), a ^ (solveGeom a t h + 1) - 1 ≥ t * (a - 1)
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmp117v7r7f/proof.olean
Finished imports
Finished replay
---
def
solveGeom
(a : ℕ) → ℕ → a > 1 → ℕ
:= fun (a : Nat) (t : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveGeom_isgeq
∀ (a t : ℕ) (h : a > 1), a ^ (solveGeom a t h + 1) - 1 ≥ t * (a - 1)
#[propext, sorryAx]

Second Theorem Proof:

theorem solveGeom_ismin(a t:Nat)(h:a>1): Not (∃ y<solveGeom a t h, a^(y+1)-1>= t*(a-1))

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmp117v7r7f/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmp117v7r7f/target2.olean
Finished imports
Finished replay
---
def
solveGeom
(a : ℕ) → ℕ → a > 1 → ℕ
:= fun (a : Nat) (t : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveGeom_ismin
∀ (a t : ℕ) (h : a > 1), ¬∃ y < solveGeom a t h, a ^ (y + 1) - 1 ≥ t * (a - 1)
#[sorryAx, propext]
------------------
Replaying /root/CodeProofTheArena/temp/tmp117v7r7f/proof2.olean
Finished imports
Finished replay
---
def
solveGeom
(a : ℕ) → ℕ → a > 1 → ℕ
:= fun (a : Nat) (t : Nat) (h : GT.gt.{0} Nat instLTNat a (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
solveGeom_ismin
∀ (a t : ℕ) (h : a > 1), ¬∃ y < solveGeom a t h, a ^ (y + 1) - 1 ≥ t * (a - 1)
#[sorryAx, propext]