Comment by Smaug123
1 day ago
I'd be interested in hearing a field report on this! For example, I can easily imagine that they're great at walking through the proof step by step, explaining background as necessary; but as TFA notes, one of the most important questions is "why is this definition the way it is?", and my bet would be that the Lean is not enough to help the LLMs meaningfully in answering that.
LLMs like even the sota flash models have great range of background math knowledge and have no problem reading and understanding flt level of math. On the other hand you don't want to go through 13 million lines of often repetitive code line by line. Models are great at synthesizing math content out of code. My contribution is to steer it through subjects of most interests to me, drill down into jargons that can be confusing, be creative in using computation for illustration (which coding agents can execute very proficiently) etc.
Fortunately LLMs are smart enough to handle that already.