Executive Summary

A bug in Lean 4’s string‑slicing function (String.Pos.Raw.extract) allowed a false proof of Fermat’s Last Theorem. The logical definition returned an empty string for a huge index, while native code returned the full string, creating a contradiction that let Lean prove any statement. The issue was reported to Trail of Bits, patched in Lean 4.34.0‑rc1, and highlights the need for careful validation of machine‑checked proofs.

---

Intelligence Metadata - Source Publisher: Trail of Bits - Published Date: 2026-09-09T11:00:00+00:00 - Category: research

Original Description: Fermat famously claimed to have a “truly marvelous proof” of his Last Theorem, but he never wrote it down, insisting the margin of his page was too narrow to contain it. A few centuries later, Anthropic announced a complete formalization of Fermat’s Last Theorem using 13 million lines of Lean code (clearly not what Fermat intended). Luckily, we found a wonderfully cursed Lean bug, shown below, that suggests the proof may have fit the margin after all. The issue affects all stable versio...

"Keep yourself to the sunshine and you cannot see the shadow."

— Helen Keller