Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • I love that “grind” is a keyword.
    by RantyDave
  • Now we have what Fermat tried to write in the margin: aa2d8b34692b16c70f699536de0d8e75b9a3e9ef
    by ks2048
  • This is a very impressive result. Bravo to that team.
    by abhv
  • Front-page discussion: https://news.ycombinator.com/item?id=49568506
    by rawling
  • Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?
    by superposeur
  • I think an interesting problem, perhaps even more interesting problem, would be the shortest / most concise / easiest to understand (formally verifiably) proof.
    by chvid
  • What a time to be alive stuff.

    https://github.com/anthropics/fermats-last-theorem/blob/main...

    by mcapodici
  • I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.

    My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)

    by black_knight

Explore Birbla archives

Fermat's Last Theorem in Lean 4 · Birbla