Submission Details

Back to Submissions List

Challenge: solve1x1

Submitted by: GasStationManager

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

Code:

import Mathlib.Data.Rat.Defs

def solve1x1(a b: Rat): Option Rat

:=sorry

First Theorem Proof:

theorem solve1x1_correct(a b:Rat): (∃ x, a*x=b) -> a * (solve1x1 a b).get! =b

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpppzo_x2j/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpppzo_x2j/target.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_correct
∀ (a b : ℚ), (∃ x, a * x = b) → a * (solve1x1 a b).get! = b
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpppzo_x2j/proof.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_correct
∀ (a b : ℚ), (∃ x, a * x = b) → a * (solve1x1 a b).get! = b
#[propext, sorryAx]

Second Theorem Proof:

theorem solve1x1_none(a b:Rat): (Not (∃ x, a*x=b)) -> solve1x1 a b=none

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmpppzo_x2j/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmpppzo_x2j/target2.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_none
∀ (a b : ℚ), (¬∃ x, a * x = b) → solve1x1 a b = none
#[propext, sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmpppzo_x2j/proof2.olean
Finished imports
Finished replay
---
def
solve1x1
ℚ → ℚ → Option ℚ
:= fun (a : Rat) (b : Rat) => sorryAx.{1} (Option.{0} Rat) Bool.false
#[propext, sorryAx]
---
theorem
solve1x1_none
∀ (a b : ℚ), (¬∃ x, a * x = b) → solve1x1 a b = none
#[propext, sorryAx]