How to start as a non mathematician

Stream: Machine Learning for Theorem Proving

[Chiung-Yi Tseng]

Hi all, I'm new to LEAN projects and community. I've been curious about leveraging AI/ML on formal proof. I feel strongly that mathematics (especially formal) is a very important step to AGI. My math background is weak and rusted, only learned about linear algebra, discrete math, abstract algebra and real analysis (badly). My AI/ML experience is limited to AI accelerators.

How may I start? Can you recommend papers/labs/researchers to pay attention to? Any tip on applying to graduate school?

[Leni Aniva]

If you want to learn Lean you can start by learning Lean via one of its textbooks or courses.

We have a couple researchers here at Stanford Centaur Lab: https://centaur.stanford.edu/courses.html

[Tyler Josephson ⚛️]

You found the ML channel on Zulip, so stick around here! I recommend this book: https://hrmacbeth.github.io/math2001/

You can also check out the course I taught on this last summer: https://github.com/ATOMSLab/LFSE2024, with lectures on YouTube: https://www.youtube.com/playlist?list=PLX21uJ4UfpF43NExUcPcAEgnzV58x_26l