Submission Details

Back to Submissions List

Challenge: GCD

Submitted by: GasStationManager

Submitted at: 2024-11-24 10:14:00

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:

Compilation error for /root/CodeProofTheArena/temp/tmpg2wc2z10/target.lean:
/root/CodeProofTheArena/temp/tmpg2wc2z10/target.lean:4:13: error: unexpected token ','; expected ')'
/root/CodeProofTheArena/temp/tmpg2wc2z10/target.lean:9:16: error: function expected at
  GCD
term has type
  ?m.53
/root/CodeProofTheArena/temp/tmpg2wc2z10/target.lean:9:34: error: function expected at
  GCD
term has type
  ?m.53

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