Ask HN: When will a technology like Lean Prover overtake LaTeX?

[Edit: Measured by it's adoption in the workflows of working mathematicians, students enrolled in math classes, etc.]

I have been typing up exercises from the end of chapter one of Atiyah and MacDonald's "Introduction to Commutative Algebra" in LaTeX (via emacs plus auctex). As a commutative algebra student, I wonder if it would be fun to type these up with software like the Lean prover (https://leanprover.github.io/about/).

Typing up proofs is reminding me that using LaTeX is already a quasi-programming experience: I tend to try to solve problems on paper, and then go type them up, but the process is never a transcription--I am editing and revising, thinking in the language of LaTeX, as I type up the hand-written proof.

If I invested the time in energy in getting somewhat conversant in Lean, I wonder if I could use it to type up my solutions to exercises at the end of Chapter 1 in Atiyah-MacDonald? I have no idea. Do you think the technology is there, or not? I'm not interested in taking on a computer science research project.