{"data":{"id":"15fdaa51-4baa-496a-8ab4-976173f2dd6d","title":"A “proof” of Fermat’s Last Theorem that fits the margin","summary":"A bug in Lean (a proof-verification software) allowed researchers to create a fake \"proof\" of Fermat's Last Theorem by exploiting a flaw in String.Pos.Raw.extract (a function that slices strings). The bug caused a mismatch between Lean's logical definition and its compiled native code, allowing contradictions that could \"prove\" false statements. The Lean team fixed the issue within hours to days of the report.","solution":"The patch is incorporated in Lean v4.34.0-rc1. The fix addressed both a memory-safety problem (merged about 3 hours after the report) and a semantic mismatch issue (fixed about 5 days after the report). Users should upgrade to v4.34.0-rc1 or later. Additionally, when validating proofs, check #print axioms to ensure no untrusted axioms (like native_decide, which includes the compiler in the trusted boundary) are present.","labels":["security","research"],"sourceUrl":"https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/","publishedAt":"2026-09-09T11:00:00.000Z","cveId":null,"cweIds":null,"cvssScore":null,"cvssSeverity":null,"severity":"medium","attackType":["other"],"issueType":"news","affectedPackages":null,"affectedVendors":[],"affectedVendorsRaw":["Lean","Anthropic","OpenAI"],"classifierModel":"claude-haiku-4-5-20251001","classifierPromptVersion":"v3","cvssVector":null,"attackVector":null,"attackComplexity":null,"privilegesRequired":null,"userInteraction":null,"exploitMaturity":null,"epssScore":null,"patchAvailable":null,"disclosureDate":"2026-09-09T11:00:00.000Z","capecIds":null,"crossRefCount":0,"attackSophistication":"advanced","impactType":["integrity"],"aiComponentTargeted":"framework","llmSpecific":false,"classifierConfidence":0.75,"researchCategory":null,"atlasIds":null}}