[majikaja]

I think an important thing for something like Lean to gain traction is the availability of learning resources (math 'textbooks') based on the technology so people actually use it for day to day mathematics instead of just formalizing what has already been proven without it.

I don't think many people are going to read Rudin (etc.) then try to rewrite the book or do the exercises in Lean by themselves or read through the mathlib files to see how everything is defined/proved in full generality.

Like a lot of people (I imagine), I'm not a professional mathematician working on advanced, complex problems but I would like to have the ability to have the computer check my solutions to exercises and maybe even aid me with hints for tackling problems if needed.

If math textbooks gave free use for people to rewrite them into computer format and post online it would make life a lot easier.

[joachimma]

Terrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean.

https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t...

[majikaja]

This is cool

I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.

[griffzhowl]

Have you tried "Mathematics in Lean"? It's in the Books section here, along with a few other resources:

https://leanprover-community.github.io/learn.html

[majikaja]

Yes I am aware of this one, it seems like a good intro.

I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?

If everything is digitalized no one will have mark homework ever again.