Submission Details

Back to Submissions List

Challenge: Falsuehood

Submitted by: GasStationManager

Submitted at: 2024-11-27 23:25:50

Code:

def not_so_empty_now : Empty :=

by
  run_tac do
    Lean.addDecl (.axiomDecl { name := `cheating, levelParams := [], type := .const `False [], isUnsafe := false })
  exact cheating.elim

First Theorem Proof:

theorem inconsistent : False :=

cheating

Status: Incorrect

Feedback:

Compilation error for /root/CodeProofTheArena/temp/tmpnj9enn0s/proof.lean:
/root/CodeProofTheArena/temp/tmpnj9enn0s/proof.lean:6:2: error: unknown constant 'Lean.Elab.Tactic.TacticM'
/root/CodeProofTheArena/temp/tmpnj9enn0s/proof.lean:12:0: error: unknown identifier 'cheating'