I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things.

As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.

▲

therobots927 5 hours ago | parent [-]

I see. So you seem to lean towards it being unlikely they would be able to use lean to evaluate this proof in an automated way…

	▲	Jweb_Guru 3 hours ago \| parent [-]
		I'm honestly not familiar enough with how well-developed graph theory is in Lean to be able to say. The paper is mostly using pretty old results, so it's mostly a matter of whether that stuff has already been formalized or not. Like anything else in software (and Lean proofs are very much software) a lot of it's about infrastructure. It wasn't so long ago that no area of mathematics outside of type theory and formal verification was really built up enough to do "serious" math -- that's changed a lot within the last few years. What I'm more saying is that we're a ways away from being able to straightforwardly go from an LLM having a paper proof to having that proof formalized in Lean in the general case. Not so much because it's hard for LLMs, more just because it's hard in general unless all that background work has already been done. As more and more of foundational mathematics gets mechanized, it will be easier and easier to check your work in Lean while you work on the proof. For example, AFAIK unit distance has already been mechanized (though the quality of the mechanization effort sounds not great, it still greatly increases our assurance in the proof's correctness).