>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.
> reduce the burden of refereeing new work.
As a professional mathematician, I rarely need to worry about the correctness of a paper. The main difficulty of writing a review is instead understanding what the results of the paper mean in its context, how the results are presented, etc.
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.
> Feel very grateful I was never taught this...
Never heard of Abstract section? First semester on a college or last year on high school.
Unfortunately I don't see this particular view paying off in the age of AI, as many prove they have nothing at all to say but say it anyways. Which isn't to say people shouldn't write if they enjoy writing, but I for one will stay a discerning reader.
Buzzard is writing for his blog audience - mostly mathematicians and not the casual visiting HN user.
Eh? The quote is from Anthropic, not Buzzard.
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.