alt Hacker NewsIs there anyone more knowledgeable than me about proof checking software who could tell me how off the mark I am here?
Assuming you have decent proof checking software, is it possible that this solution was achieved by throwing GPT at the problem a couple hundred thousand times until it passed the proof checker?
Replies
As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.
Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.
The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.
At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.
On the last Dwarkesh podcast with 3blue1brown, one of them mentioned that frontier models are now able to work through a whole proof in natural language, just like a human mathematician would. But when they first solved IMO problems in 2024, they relied more on Lean to catch hallucinations.
As someone who's used proof checkers a fair amount, if you don't have some high level idea about the proof, it's an open problem, and the hard part isn't some extremely tedious finite case analysis, it's extremely unlikely you'll get anywhere by trying to mechanize by throwing stuff against the wall to get it to typecheck. When people talk about mathematics being a closed formal system as though this trivializes any creative component, what they're omitting is that in type theory like that used by Lean or Rocq, there are two kinds of terms (match statements proving dependent elimination and fixpoints that provide proof by induction) where there's no real way to infer the type from the term. i.e., there are cases where you have to get creative and try to prove something more general than what you actually care about in order to get the proof about the original case to go through. What does "more general" mean? It could mean anything... that's the problem. That's why it's usually advantageous to reformulate the problem in terms of a different abstraction and build on top of existing results, knowing a lot about the literature and the way these kinds of problems tend to be attacked, rather than just chuck random terms over to a proof assistant and hope for the best.