Submission Details

Back to Submissions List

Challenge: Falsuehood

Submitted by: GasStationManager

Submitted at: 2024-11-27 23:29:21

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

import Mathlib.Tactic
/- retrying eric wieser's entry -/

First Theorem Proof:

theorem inconsistent : False :=

cheating

Status: Incorrect

Feedback:

found a problem in /root/CodeProofTheArena/temp/tmphws7mj6t/proof.olean
uncaught exception: cheating is not in the allowed set of standard axioms
------------------
Replaying /root/CodeProofTheArena/temp/tmphws7mj6t/target.olean
Finished imports
Finished replay
---
def
not_so_empty_now
Empty
:= sorryAx.{1} Empty Bool.false
#[sorryAx]
---
theorem
inconsistent
False
#[sorryAx]
------------------
Replaying /root/CodeProofTheArena/temp/tmphws7mj6t/proof.olean
Finished imports
Finished replay
---
def
not_so_empty_now
Empty
:= False.elim.{1} Empty cheating
#[cheating]
---
theorem
inconsistent
False
#[cheating]