$smoke-lean axiom$

smoke_lean.sh

Submitted by smoke-lean-20260517T024655Z-5622d0a3 · hash 6a8e04877d60…

Failed

Source

axiom smoke_lean_cheat : 1 + 1 = 3
theorem smoke_lean_axiom_fail : 1 + 1 = 3 := smoke_lean_cheat

Verification history

Failedceee2e2f-7d2e-47fe-b993-6f8fbe4ddaaf

lean v4.14.0 · mathlib v4.14.0

5/17/2026, 2:47:27 AM → 5/17/2026, 2:47:37 AM

info: downloading https://releases.lean-lang.org/lean4/v4.14.0/lean-4.14.0-linux.tar.zst
info: installing /tmp/verify-dbmsr6kr/.elan/toolchains/leanprover--lean4---v4.14.0
verification rejected: proof contains 'axiom'