Submission Details

Back to Submissions List

Challenge: GCD

Submitted by: GasStationManager

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

Code:

def GCD(a b:Nat):Nat

:=sorry

First Theorem Proof:

theorem gcd_is_div (x y: Nat):
  (p: x > 0)→ ((GCD x y) ∣ x) ∧ ((GCD x y) ∣ y)

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmphnnwwdw5/proof.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmphnnwwdw5/target.olean
Finished imports
Finished replay
---
theorem
gcd_is_div
∀ (x y : ℕ), x > 0 → GCD x y ∣ x ∧ GCD x y ∣ y
#[sorryAx]
---
def
GCD
ℕ → ℕ → ℕ
:= fun (a : Nat) (b : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmphnnwwdw5/proof.olean
Finished imports
Finished replay
---
theorem
gcd_is_div
∀ (x y : ℕ), x > 0 → GCD x y ∣ x ∧ GCD x y ∣ y
#[sorryAx]
---
def
GCD
ℕ → ℕ → ℕ
:= fun (a : Nat) (b : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]

Second Theorem Proof:

theorem gcd_is_greatest (x y: Nat):
  (x>0) → Not (∃ z: Nat, z∣ x ∧ z∣ y ∧ z> GCD x y )

:=sorry

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmphnnwwdw5/proof2.olean
uncaught exception: sorryAx is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmphnnwwdw5/target2.olean
Finished imports
Finished replay
---
def
GCD
ℕ → ℕ → ℕ
:= fun (a : Nat) (b : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
gcd_is_greatest
∀ (x y : ℕ), x > 0 → ¬∃ z, z ∣ x ∧ z ∣ y ∧ z > GCD x y
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmphnnwwdw5/proof2.olean
Finished imports
Finished replay
---
def
GCD
ℕ → ℕ → ℕ
:= fun (a : Nat) (b : Nat) => sorryAx.{1} Nat Bool.false
#[sorryAx]
---
theorem
gcd_is_greatest
∀ (x y : ℕ), x > 0 → ¬∃ z, z ∣ x ∧ z ∣ y ∧ z > GCD x y
#[sorryAx]