Hacker GitHub

← All repos

ImperialCollegeLondon/FLT

View on GitHub ↗ ★ 1,056 Lean

Ongoing Lean formalisation of the proof of Fermat's Last Theorem

9 mentions on Hacker News by 8 people: 2 stories, 7 comments · first 2024-12-12 · latest 2026-09-04

Mentions per year 9 mentions · busiest year 2025 (5)
20082026
AllStoriesComments NewestTopOldest
  1. Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT
    comment by kdavis · 2026-09-04 · in Formalizing Fermat's Last Theorem
  2. …mathematician and AI doesn't answer very well. Could someone tell us how big an endeavour this is: https://github.com/ImperialCollegeLondon/FLT ? (the site is : "An ongoing multi-author open source project to formalise a proof of Fermat's…
    comment by wiz21c · 2026-07-28 · in Solving Fermat: Andrew Wiles
  3. https://github.com/ImperialCollegeLondon/FLT
    comment by williamstein · 2026-05-10 · in A recent experience with ChatGPT 5.5 Pro
  4. ▲ 2
    A Lean Formalisation of Fermat's Last Theorem
    story by bcye · 2025-09-04 · 0 comments
  5. …a year to patch the proof. There are multiple reasons for formalizing the proof in Lean ... see https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER... P.S. "So that patching is exactly what I’m referring to." No, it isn't. "The…
    comment by jibal · 2025-08-21 · in Project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover
  6. https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER... "It will not be the original Wiles/Taylor-Wiles proof, but rather a "newer" proof which takes into account more recent developments due to Khare-Wintenberger, Kisin and many…
    comment by jibal · 2025-08-21 · in Project to formalise a proof of Fermat’s Last Theorem in the Lean theorem prover
  7. This is a nice overview of what this is, why they're doing it and why it's many years of work: https://github.com/ImperialCollegeLondon/FLT/blob/main/GENER...
    comment by seanwilson · 2025-08-03 · in Ongoing Lean formalization of the proof for Fermat's Last Theorem
  8. ▲ 127
    Ongoing Lean formalization of the proof for Fermat's Last Theorem
    story by anonyonoor · 2025-07-31 · 79 comments
  9. If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M... Also check out the blueprint, which describes the overall structure of the code:…
    comment by lincolnq · 2024-12-12 · in Fermat's Last Theorem – how it’s going