4 ms·
> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that
by m_w_ 27d ago
> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems.
Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model.
- jameshart 27d agoThere is no way Fermat could have fit that in the margin. Definitely vindicated.
- bananaflag 27d agoI am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
- HappyPanacea 27d agoIt seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.
- bananaflag 27d agoYeah Vandiver was on my mind, this is why I said 1920. Wouldnt mind it more complicated, but with simpler concepts and most importantly concepts that feel like they have something to do with FLT (cyclotomic fields, not modular forms).
- arjie 26d agoI read an interesting take that it won’t. Because it won’t be interesting any more. It’s like how no one talks about AI IMO Gold anymore or Stockfish being better than all humans. This kind of mathematics goes back to being a curiosity of humans and machines move to the next frontier. In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday. Enjoyed that idea. Not sure how true but it was enjoyable.
- zamadatix 27d agoWhile pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.
- vlovich123 27d agoGiven the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin. My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
- BeetleB 27d agoMost likely an error. Some time after he wrote that margin note, he wrote a document proving a special case of the FLT (i.e. it's true for n satisfying some property). Why would he do that if he had already proved it?
- zamadatix 27d agoI think that point actually agrees with GP's take (joking/lying about having had a proof too big to fit in the margin): He would do that because if he thought the problem was extremely difficult but didn't actually have a proof when writing the note he would still want to go on and try to pick away at the problem.
- zamadatix 27d agoMaybe, we'd have to go back and ask him to be sure. I mostly just didn't want to leave an as of yet certainly unproven vindication about this hanging in a thread about finally having a formalized proof of the star topic :D
- NooneAtAll3 27d ago> Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin. https://xkcd.com/1381/ https://xkcd.com/1381/
- avodonosov 27d agoAnd he was right to call it marvelous.
- egl2020 27d agoMaybe we need "de Moura complexity": the shortest Lean proof of a theorem.
- andriy_koval 27d agoespecially compared to existing 129 pages proof by human
- dist-epoch 27d agoInsert meme with 200 pages needed to prove 1+1=2 rigurously
- deleted 27d ago[deleted]
- black_knight 27d agoA human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.
- andriy_koval 27d ago> I am sure a lot of this development was formalising the prerequisites How can you be so sure its not result of inefficiency?
- black_knight 27d agoOh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies. I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
- itishappy 27d agoA published formalization is code. I would not think humans have any edge when it comes to citing previously published results.
- Jaxan 27d agoWouldn’t a lot already be in leans mathlib?
- kccqzy 27d agoThe next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us.
- Smaug123 26d agoYou don’t necessarily want concision for that. You want “the right abstractions”, with an API that admits nice general work building on top of it. That might mean doing things in more generality than you wanted to. For example, for a long time (and possibly even now, I’m not up to date) there was very little graph theory in mathlib because there wasn’t consensus about what “the right definition” of a graph was, to permit all the possible consumers to get what they need from the API.
- make3 26d agoInteresting. Indeed, proving theorems that are stronger and more general "accidentally" than what you really need is not a bad thing.
- skobes 27d agoMaybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct? How have we not merely substituted one verification problem for another?
- Legend2440 27d agoThe point of Lean is that it can be mechanically verified by a proof checker.
- sashank_1509 27d agoNot always, there can be bugs in lean. Recently some guy with claimed to disprove Collatz conjecture, only to turn out that there was a bug in lean. I actually have no idea, how anyone can be sure this 13 M lines is meaningful
- make3 26d agoLean is adversarial in a way. Lean is better thought of as a constraint language with a verifier that checks if the constraints are respected, than a programming language. Your job or the LLM's job is to write code that Lean is satisfied with, creating the link between what you're trying to prove, and mathematical axioms. If you write a bad proof, the Lean constraint checker will tell you, unless there are bugs in Lean itself, or you defined the goal constraint incorrectly.
- thaumasiotes 27d ago>> Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. > Pretty insane. I don't think the count of "intermediate theorems" tells you anything. Here's something from an algebra textbook: --- Let G be a group, let H be a subgroup [of G], and let N be a normal subgroup [of G]. Then H ∨ N = HN = { hn | h ∈ H, n ∈ N }. --- This says that the subgroup closure of H and N, the smallest subgroup that contains them both, is identical with the set consisting of all products of an element of H (on the left) and an element of N (on the right). Part of the proof: --- Suppose that x and y are elements of [the set of products hn]. Then x = h₁n₁ and y = h₂n₂, where hᵢ ∈ H and nᵢ ∈ N. Now h₂⁻¹n₁h₂ = n₃ ∈ N, as N is normal in G. So n₁h₂ = h₂n₃. In this case xy = (h₁n₁)(h₂n₂) = (h₁(n₁h₂)n₂) = (h₁(h₂n₃)n₂) = (h₁h₂)(n₃n₂), which shows that xy has the correct form. --- This will translate directly into lean. If you do it this way, you will prove at least 10 of what would be described in lean as 'intermediate theorems': ∃ h₁ ∈ H, ∃ n₁ ∈ N, x = h₁ * n₁ ∃ h₂ ∈ H, ∃ n₂ ∈ N, y = h₂ * n₂ h₂⁻¹ * n₁ * h₂ ∈ N n₁ * h₂ = h₂ * n₃ x * y = (h₁ * n₁) * (h₂ * n₂) (h₁ * n₁) * (h₂ * n₂) = (h₁ * (n₁ * h₂) * n₂) (h₁ * (n₁ * h₂) * n₂) = (h₁ * (h₂ * n₃) * n₂) (h₁ * (h₂ * n₃) * n₂) = (h₁ * h₂) * (n₃ * n₂) h₁ * h₂ ∈ H n₃ * n₂ ∈ N But none of these would be called an "intermediate theorem" in a paper proof.
- gus_massa 26d agoIt looks like an exercise for a course in "Algebra 2" in my university. (A different course name in other universities.) I probably should know it. Give me 30 minutes to prove it. (Part of the magic is in "normal".) My algebraic friends surely know it and they would never include it in a paper because everyone knows it. I'm surprised it's not in mathlib. Perhaps it is and the AI made a copy. Perhaps it isn't and it is a nice PR for beguiners.
- thaumasiotes 26d agoIt is in mathlib. In textbooks it's presented as an introductory part of the Second Isomorphism Theorem; in mathlib it's here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Subgroup/Pointwise.html#Subgroup.coe_mul_of_left_le_normalizer_right https://leanprover-community.github.io/mathlib4_docs/Mathlib... . The part of the proof that I quoted just proves that the product set HN is closed under multiplication - the product of any two elements in HN is also an element of HN. This is part of proving that HN is a subgroup. You might call it an 'intermediate theorem' to that proof. My point isn't that this is missing from mathlib, or that this result is part of the work mentioned in the blog post. It's that doing this proof in a way that matches the textbook proof requires you to prove a large number of "intermediate theorems", and that those "intermediate theorems" often look more like computational steps than anything that a mathematician might call "theorems". In particular, note that the 10 required intermediate theorems I mentioned all refer to free variables.
- newAccount2025 27d agoIt’s common for formal proof efforts about software and hardware to involve thousands to tens of thousands of small lemmas. 13M lines does seem extreme and there is probably a lot of inefficiency given the way the proof was developed. Cutting it down is probably a long road, but is also a very well defined problem that AIs can probably just go do with enough time and budget now.