Re:I struggle to believe that AI R&D is ingenious
by internet_points on Friday November 06, 2026 @03:38AM
(#50389701)
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.
Re:I struggle to believe that AI R&D is ingenious
by ogogmad on Friday November 06, 2026 @04:51AM
(#50390318)
In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. What they're truly bad at is explaining their proofs. Until they improve at that, we'll have to keep asking Lean whether they solved something correctly.
While they're not great at explaining their own proofs, some models are good at explaining older, human-written proofs.
Re:I struggle to believe that AI R&D is ingenious
by ccppurcell on Saturday November 07, 2026 @08:13AM
(#50404295)
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.
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.