Ask HN: Is AI good enough for math exercises?

[Qision]

Hi, I need to brush-up and deepen my math knowledge at undergrad level.

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.

[hackermailman]

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

[Qision → hackermailman]

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

[hackermailman → Qision]

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).

[gus_massa]

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.