Yeah, I think it’s going to improve a lot. Though, I actually think the Lean proofs only provide so much benefit.

The LLMs operate in a lot of ways remarkably similarly to how we do. It’s just as important for them to be able to “chunk” ideas into coherent blocks as it is for us. Lean code still allows writing what I would describe as spaghetti-code proofs, and doesn’t require building your theory with the sort of coherent building blocks that lets you build high.

I think the real improvements will come as we learn to use LLMs to write more structured and elegant proofs, and at least for the near term, I think that that favors the human language approach over the Lean-first approach.

I’m definitely not totally confident of this, and wouldn’t be shocked to be wrong though.