Fermat claimed to have a proof for his Last Theorem too large for his notebook margin. Recently, a formalization of Fermat's Last Theorem in Lean code resulted in a bug. This bug was discovered while experimenting with AI for code review. The issue affects how Lean's string slicing function handles extremely large positions. Logically, it should return an empty string, but compiled code returns the original string. This discrepancy creates a contradiction. The theorem prover mistakenly concludes the empty string equals a non-empty string. This allows for any statement to be proven, including Fermat's Last Theorem. The Lean team fixed the bug remarkably quickly after it was reported. The fix involved addressing both memory safety and semantic mismatches. While machine-checked proofs offer great trust, vulnerabilities can arise from theorem prover issues. Careful validation of Lean proofs is therefore essential.