公理を書き換えて任意の命題を示せてしまう例。偽証明の例。

Zulip: https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Code.20with.20Proofs.3A.20the.20Arena/near/482808260

import Batteries.Tactic.OpenPrivate

/- Redefine `propext : False`. -/
open Lean Elab Meta in
open private Environment.mk from Lean.Environment in
#eval modifyEnv (m := MetaM) fun env =>
  let consts :=
    { env.constants with
        map₁ := env.constants.map₁.insert ``propext (.axiomInfo {
          name := ``propext
          type := .const ``False []
          levelParams := []
          isUnsafe := false
        })
    }
  Environment.mk env.const2ModIdx consts env.extensions env.extraConstNames env.header

theorem efsq : ∀ (x y z n : Nat),
    0 < x → 0 < y → 0 < z → 2 < n →
    x^n + y^n ≠ z^n := by
  exfalso
  exact propext

-- 'efsq' depends on axioms: [propext]
#print axioms efsq

Start by reading the linked Zulip discussion and reproducing the Lean snippet in the issue. The issue does not name a repository file, test, or requested change; completion would require a maintainer decision about whether this behavior is a bug and what remedy or documentation is appropriate.