>But maybe that’s still just making the proof easier for humans to understand? No! For one, this usually makes the proof shorter, and sometimes dramatically shorter.

Hmm, so is the way to train this to take all the long complicated proofs it generates in Lean and then use autoresearch to minimize the length of the proof?

My priors have been so thoroughly updated by all the recent progress in AI that it really seems like there isn't anything that fundamentally cannot be learnt. So, is this how we train this kind of taste?

I'm not a mathematician, nor an AI engineer/researcher. Just watching from the sidelines and spitballing ideas.

What a time to be alive?