A “Proof” of Fermat’s Last Theorem That Fits the Margin

[carlospolop]

🤖 Automated Content Update

This PR was automatically generated by the HackTricks News Bot based on a technical blog post.

📝 Source Information

• Blog URL: https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin
• Blog Title: A “Proof” of Fermat’s Last Theorem That Fits the Margin
• Suggested Section: Generic Hacking > Proof Assistant and Formal Verification Security (new subsection)

🎯 Content Summary

Overview. The post demonstrates a false but apparently checked proof of Fermat’s Last Theorem in Lean. It contrasts this tiny proof with Anthropic’s complete formalization, which used approximately 13 million lines of Lean code. The proof exploits a bug in String.Pos.Raw.extract, Lean’s low-level string-slicing function. The issue affects all stable Lean versions through 4.33.1; the patch is included in v4.34.0-rc1. The bug was tracked i...

🔧 Technical Details

Logical/native differential evaluation. In a proof assistant or verified runtime that offers both a logical evaluator and a compiled/native evaluator, test boundary cases involving enormous indexes, one-byte lengths, empty values, and out-of-range positions. If the logical definition and native implementation disagree, the same expression can be assigned two different values by two trusted evaluation paths.

Turning evaluator disagreement into arbitrary proof. If a compiler-backed decision procedure such as native_decide can import native execution results into the logic, combine a logically reduced result with the contradictory native result. Proving that the same expression equals two different values yields False; the proof assistant’s explosion principle can then derive any target proposition, including false mathematical or verification claims.

Auditing compiler-expanded trust boundaries.🤖 Agent Actions

Implemented the HackTricks update:

• Added proof-assistant-formal-verification-security.md under Generic Methodologies.
• Documented:
  • Logical/native differential evaluation.
  • Boundary-value testing for runtime primitives.
  • Turning evaluator disagreement into False.
  • Lean native_decide trust-boundary expansion.
  • Auditing with #print axioms.
  • Validation using lean4checker and lake comparator.
• Added numbered references to the original Lean issue, fix PR, official validation guidance, and Trail of Bits post.
• Linked the page from SUMMARY.md and the existing differential-fuzzing section.

Validation passed with git diff --check and custom structural/link checks. mdbook was not installed, so a full build was unavailable.

---

This PR was automatically created by the HackTricks Feed Bot. Please review the changes carefully before merging.

[carlospolop]

🔗 Additional Context

Original Blog Post: https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin

Content Categories: Based on the analysis, this content was categorized under "Generic Hacking > Proof Assistant and Formal Verification Security (new subsection)".

Repository Maintenance:

• MD Files Formatting: 1033 files processed

Review Notes:

• This content was automatically processed and may require human review for accuracy
• Check that the placement within the repository structure is appropriate
• Verify that all technical details are correct and up-to-date
• All .md files have been checked for proper formatting (headers, includes, etc.)

Bot Version: HackTricks News Bot v1.0