alt Hacker NewsI think it does gel. You're right that the comment you're replying to is weakened by that fact.
It gels because they solved about 700 problems out of 4000 attempts. And they threw a ton of resources at each. So "per problem" it's less than 1 in 5, "per token" it's probably not a great record. I mean it's astonishing that it's possible at all of course. But on average, even an expert with a top model will probably have an underwhelming response to the vast majority of prompts.
and I'm guessing it was with "tool calling" ie. they can write a bunch of Lean proofs and hit compile and basically brute-force a whole bunch of hypotheses quickly?
Ie. the LLM itself isn't as "smart" as the combination of LLM, Lean, looping, search and vast gpu/cpu-time.