But ask them to enumerate all the intermediate steps required to create a formal direct proof, and it will loose attention and forget important details as they go out of their input window size. You need to combine them with a proper logical problem solver to get the best parts of both.
It's interesting how people will comment on LLM capabilities despite clearly not having engaged with frontier models in any meaningful way in a long time
Having models write Lean proofs of mathematical claims is standard operating procedure for any LLM math discovery!
The proofs will be only as good as the framework for linking successive instances of reasoning.
Proofs stretching thousands of pages are split into lemmas, grouped into sub theories.
What I haven’t seen agents do yet is to develop new ideas for entire such theories. I have usually seen them bite into some existing idea and grinding out related results. But I am less sure than ever that they won’t!
The codebase you describe would be an external tool in GP's conception.