I plan to work from books (Tao's Analysis, Spivak etc.) and ask an AI to correct my solutions to exercises (not do the teaching). I have access to Gemini Pro and a Macbook M5 so maybe a Qwen version should run locally.
Do you think AI is good enough for such a task? Or should I expect some mistakes in reasoning and/or hallucinations? I am not super good at proofs and I'd like to improve. I would appreciate any feedback from anyone who had similar experience.
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
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).
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.