

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.








Honestly, it already looks ridiculous.
To be clear, I think the automation of jobs is, at least in the immediate, a serious problem, with real consequences. The problem is real. The issue is that objecting to the technology itself is idiotic. That’s not a fight you’ll win. The technology exists. People are going to use it. And in the long run we’ll all be better off for it.
There’s serious conversations to be had about how we use AI, and how we deal with the consequences of its use, and especially how we manage the transition. But you can’t have those conversations with someone who insists that AI is the devil and that we need to stop it, and who gets mad at you when you suggest otherwise.