Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?