points by ccppurcell 2 days ago | 0 comments
I 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.
[–] internet_points 2 days ago
[–] ogogmad 2 days ago
In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. That last step sometimes takes them much longer than checking their proof without Lean, which is a problem humans have as well. What they're truly bad at, however, is explaining their proofs. Until they improve at that, we'll have to keep resorting to Lean to check whether they solved something correctly.
I'm less sure about the following, however: I think that while current LLMs are bad at explaining their own proofs, some models are great for discussing older, human-written proofs. For this use case, from best to worst, Gemini > Claude > GPT-Astra >>>>>>>>>>>> GPT-Sol.
[–] ccppurcell 23 hours ago
I definitely don't know but I got the impression it's the opposite. Based on the observations about Navier Stokes and the natural language proof not matching up with the lean proof and other things. They generate lean and convert it into natural language at the end. But really I could be wrong just giving anyone interested a lead to check out.
Ie. the LLM itself isn't as "smart" as the combination of LLM, Lean, looping, search and vast gpu/cpu-time.