Comment by sigmar
10 hours ago
>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.
Forgive the authors of the article for assuming readers would complete it.
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?
Feel very grateful I was never taught this... Would have missed out on quite a lot of good bodies of text in my life I think! Pushing through any initial friction or ignorance I might have as a reader, having the patience and charity to bear with an author until you get it, was instead what I was always taught.
Giving such a blanket "responsibility" to the author at all is just such a bummer! I say let them do whatever they want, there is always more than one way to express oneself. Someone who was never taught to write a clear thesis in the first paragraph for whatever reason doesn't inherently have less to say.
2 replies →
Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.
1 reply →
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.
They said 6 billion tokens, which isn't as much as I thought it might be.
Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.
Nah they should have released it in a 14-part tweet instead.