It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.

cvoss 2 hours ago | parent | next [-]

Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.

Panoramix 5 hours ago | parent | prev [-]

How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.

	▲	kenferry 2 hours ago \| parent \| next [-]
		Well, the point of the _computer_ formalization is that it's checkable. An error in the formalization would be a bug in lean. Which, as we know, certainly seems plausible (I've mused on if these giant proofs are incentivizing LLMs to find lean bugs to exploit), but at least it's a smaller surface area.
	▲	sebzim4500 4 hours ago \| parent \| prev [-]
		In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify. In this case the statement is unusually complicated but still much much easier to verify than the proof itself.