alt Hacker News>The speed with which we were able to produce this proof demonstrates that it is now possible to formalize large swaths of mathematics, which may both catch errors in the common body of mathematical proofs and reduce the burden of refereeing new work.
^ this section should have been in the first few paragraphs imho. Explaining why this is relevant shouldn't be so far down.
Replies
doctoboggan • today at 9:47 PM
Isn't it the cost we care about, rather than the speed? All we know know is that a frontier AI lab was able to do it in 11 days, we have no idea how much compute they threw at it.
paxys • today at 8:29 PM
Nah they should have released it in a 14-part tweet instead.
Forgive the authors of the article for assuming readers would complete it.