---
id: 7556
title: "A “proof” of Fermat’s Last Theorem that fits the margin"
source_domain: blog.trailofbits.com
source_url: "https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/"
published_at: "2026-09-09T11:00:00Z"
tags: ["memory-safety", "vulnerability", "formal-verification", "trail-of-bits", "lean", "mathematics"]
phying_url: "https://phying.com/item/7556"
lang: en
---

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

## Summary

Trail of Bits found a Lean ≤4.33.1 bug: String.Pos.Raw.extract returns a full string where its spec says empty — enough to 'prove' Fermat's Last Theorem. Not a soundness flaw; fixed in 4.34.0-rc1.

## Intelligence Metadata

- **Sources:** blog.trailofbits.com
- **Published:** 2026-09-09T11:00:00Z
- **Original:** https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/
- **Phying News:** https://phying.com/item/7556