OpenAI says an unreleased Astra found 10 math/CS results, each turned into Lean proofs, because plain claims are so last decade.
4 comments
Feels like Flyspeck, just with a broader search loop.
Lean can force extra hypotheses, so the search loop isnt the whole cost.
> Lean can force extra hypotheses, so the search loop isnt the whole cost.
Sure, but that feels like a side effect, not the main story. The expensive part is still finding a statement worth proving in the first place, and Lean mostly changes the cost of checking and tightening the argument after that.
If anything, the proof assistant makes the comparison cleaner, because it stops people from hand-waving about what the model
I wouldnt call Lean just a side effect here, because in the article they say humans used the same model to turn the arguments into machine-checkable proofs. That means the real output isnt only a candidate statement, its a statement that survives the typechecker, which is a pretty different bar than Flyspeck style informal search.
The part people skim past is the 249-page manuscript plus proof files, those let you separate invention from polishing. If a model can spit out a plausible theorem and then keep enough structure around for Lean to accept it, thats a lot closer to a usable theorem-finding loop than just a broader brute-force search.