Skip to content

Back to the catalog

A “proof” of Fermat’s Last Theorem that fits the margin
blog.trailofbits.comwriteup

A “proof” of Fermat’s Last Theorem that fits the margin

Trail of Bits found a bug in Lean's String.Pos.Raw.extract (affecting all stable versions up to 4.33.1, fixed in 4.34.0-rc1) where the logical definition and the compiled native code disagree on the result of extracting a slice at an out-of-bounds position, letting an attacker manufacture a contradiction (empty string = non-empty string) that "proves" any theorem, including a fake formalization of Fermat's Last Theorem. The exploit only works when a proof relies on the native_decide axiom, which extends trust to the compiler rather than the kernel; the researchers found the issue while using GPT-5.6 to build a code-review skill, and Lean maintainers hargoniX and Rob23oba shipped fixes within hours to days of disclosure. The post is a reminder that machine-checked proofs are only as trustworthy as the evaluator/compiler paths behind axioms like native_decide, and points to work like lean4lean and alternative kernels as mitigations.

TL;DR Trail of Bits exploited a Lean evaluator/native-code mismatch in String.Pos.Raw.extract to "prove" a fake Fermat's Last Theorem via the native_decide trust-boundary axiom.
Open original ↗
Document

What it is

A soundness-adjacent bug in String.Pos.Raw.extract, Lean 4's low-level string-slicing function, disclosed by Trail of Bits. It lets a crafted proof derive a contradiction and thereby "prove" any theorem — demonstrated with a bogus proof of Fermat's Last Theorem. It affects all stable Lean versions up to 4.33.1; the patch ships in v4.34.0-rc1 (a detail the summary omits).

How it works

Ask extract for a one-byte slice at an astronomically large position. Lean's logical definition returns the empty string; the compiled native code returns the entire original string. That disagreement lets you assert the same slice is both empty and non-empty, giving "" == "a truly marvelous proof". From that contradiction, anything follows. The contradiction only enters a proof through the native_decide tactic, which adds the compiler to the trusted computing base.

Preconditions / Affected

Matters only when you accept external Lean proofs and treat a native_decide-backed proof as valid. It is explicitly not a kernel soundness issue — the ordinary kernel evaluator alone does not exhibit the mismatch; the exploit requires native_decide (the compiler path) to disagree with the logical definition.

What to do

  • Upgrade to Lean v4.34.0-rc1 or later.
  • When validating any external proof, inspect its axiom dependencies. The page shows the tell: a proof carrying this bug reports a native_decide axiom, e.g.
#print axioms flt
'flt' depends on axioms: [propext, Classical.choice, Quot.sound, flt._native.native_decide.ax_1_1]

Treat any dependency on a native_decide axiom as trusting the compiler, and audit accordingly.

Caveats

The fix landed in two stages: hargoniX patched the memory-safety half ~3 hours after the report, but the underlying semantic mismatch was only closed five days later by Rob23oba — so intermediate builds may have patched the crash without fully resolving the logical divergence. The report also notes that native_decide remains inherently compiler-trusting; the broader mitigation is defense-in-depth via independent kernel implementations (the page names lean4lean), not this single patch.

Organisations named here

  • hargoniX
  • native_decide
  • Rob23oba
  • String.Pos.Raw.extract

Technologies named here

  • Lean
  • GPT-5.6
  • lean4lean
  • #print axioms
  • Claude

Techniques named here

  • Logical/native evaluation mismatch exploitation

Related in AppSec