A “proof” of Fermat’s Last Theorem that fits the margin
A Lean bug in String.Pos.Raw.extract causes native code to disagree with the logical kernel, allowing proofs of false statements like Fermat's Last Theorem. The vulnerability stems from a divergence between Lean's kernel evaluator and compiled native code when handling astronomically large string positions. By exploiting this mismatch via the native_decide tactic, a user can derive a logical contradiction, proving arbitrary theorems. The issue affects Lean versions up to 4.33.1 and was patched in v4.34.0-rc1.
Detection / Hunteropenrouter
Immediate Actions
- Update Lean to v4.34.0-rc1 or later to resolve the soundness issue.
- Audit existing Lean proofs for dependency on the native_decide axiom.
Key Takeaways
- Bug allows proving false theorems by exploiting native_decide and string slicing mismatch.
- Affects Lean stable versions up to 4.33.1; fixed in v4.34.0-rc1.
- Root cause is a disagreement in String.Pos.Raw.extract at large positions.
- Lean team patched the memory-safety issue in 90 minutes; full fix took five days.
- Proof relies on the native_decide axiom, which trusts the compiler.
Attack Chain
- Vulnerability: Lean's String.Pos.Raw.extract returns empty string in kernel but full string in native code at large positions.
- Exploitation: User defines a theorem using native_decide to trigger the native code path.
- Contradiction: Kernel evaluates slice as empty; native evaluates it as non-empty.
- Impact: Contradiction allows proving arbitrary false theorems, including Fermat's Last Theorem.
Affected Systems
- Lean proof assistant versions up to 4.33.1
Detection Availability
No detection rules or queries are published in the source article.
Detection Engineering Assessment
Hypotheses are starting points derived from the article, not findings about your environment; validate against your own telemetry.
| Dimension | Rating | Rationale |
|---|---|---|
| EDR Visibility | None | Issue is a logic bug within a developer tool, not malware or system exploitation. |
| Network Visibility | None | No network activity or C2 communication is involved in this vulnerability. |
| Detection Difficulty | Hard | Requires auditing Lean proof dependencies and axioms, not standard security telemetry. |
Hunting Hypotheses
| Hypothesis | Telemetry | Stage | FP Risk |
|---|---|---|---|
| Hunt for Lean proofs utilizing the native_decide tactic, which expands the trusted boundary to include the compiler. | Lean proof files and CI build logs | Execution | Medium — native_decide has legitimate uses in performance-critical proofs. |
Required Log Sources
- Lean proof audit logs
- CI/CD pipeline build logs
Key Behavioral Indicators
- Lean proofs depending on the native_decide axiom
- Use of String.Pos.Raw.extract with large position values
Control Gaps
- Static analysis tools for Lean proof axiom dependencies
- CI/CD pipelines lacking Lean proof validation steps
False Positive Assessment
Low — The vulnerability requires specific Lean code patterns using native_decide and large string positions.
Recommendations
Suggestions to evaluate against your own environment, tooling, and incident-response procedures — not directives.
Infrastructure Hardening
- Enforce strict validation of external Lean proofs before integration.
- Restrict the use of native_decide in CI/CD pipelines for critical proofs.
User Protection
- Train developers on the risks of expanding the trusted boundary with native_decide.
Security Awareness
- Promote awareness of theorem prover soundness issues within development teams.
Plain-Language Summary
Researchers found a bug in Lean, a software tool used to mathematically prove code is correct. The bug makes the tool's internal logic disagree with its compiled code when handling very large text positions. This disagreement allows someone to trick the tool into saying a false statement is true, like claiming to have a short proof of Fermat's Last Theorem. Users should update Lean to version 4.34.0-rc1 or later and carefully check external proofs.
Additional IOCs
- File Paths:
RandomSystems > flt.lean- PoC file path shown in screenshot
- filenameRandomSystems>flt.leanPoC file path shown in screenshot