If you've never used Lean try some of this https://hrmacbeth.github.io/math2001/ you will eventually just pick it up then can start understanding Mathlib abstract tactics.
There's modern analysis books too for example this teaches a simpler version of what is sometimes called the Guage integral or Henstock-Kurzweil integral. Then you don't have to waste time with 'improper integrals'. https://classicalrealanalysis.info/Free-Downloads.php it has solutions and hints
Do you think it is long to learn enough Lean to do the exercises? I never used it and I don't need it at work so I don't know if it's really something I need
Up to you but since AI is firing out proofs in Lean why not learn it unless you want to unplug and do it all by hand. It doesn't matter.
Lean is a proof assistant to verify your own work and if you know basic types in programming it will be trivial to pick it up as Tao will give a template to work with. Then AI or Tao's book can tell you what the tactics mean like 'by rfl' (reflexive equality).
You can use Lean with Tao's book https://github.com/teorth/analysis
If you've never used Lean try some of this https://hrmacbeth.github.io/math2001/ you will eventually just pick it up then can start understanding Mathlib abstract tactics.
There's modern analysis books too for example this teaches a simpler version of what is sometimes called the Guage integral or Henstock-Kurzweil integral. Then you don't have to waste time with 'improper integrals'. https://classicalrealanalysis.info/Free-Downloads.php it has solutions and hints
Do you think it is long to learn enough Lean to do the exercises? I never used it and I don't need it at work so I don't know if it's really something I need
Up to you but since AI is firing out proofs in Lean why not learn it unless you want to unplug and do it all by hand. It doesn't matter.
Lean is a proof assistant to verify your own work and if you know basic types in programming it will be trivial to pick it up as Tao will give a template to work with. Then AI or Tao's book can tell you what the tactics mean like 'by rfl' (reflexive equality).
Yes.
For short exercices with clear goals, AI is super good.
For long open ended tasks, you have to steer it and/or pay $15,000,000.