>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.

▲

t_gamer_kle 2 hours ago | parent | next [-]

Forgive the authors of the article for assuming readers would complete it.

▲

salomonk_mur 2 hours ago | parent [-]

For any body of text (or in general, any exposition of any kind), the responsibility to explain the value of the article is very much in the author's side.

Explaining the value of what you are showing should always go towards the start. Else, why would anyone bother with the rest?

	▲	HappyPanacea 15 minutes ago \| parent [-]
		Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.

▲

doctoboggan 19 minutes ago | parent | prev | next [-]

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 2 hours ago | parent | prev [-]

Nah they should have released it in a 14-part tweet instead.