Share your Lean learning journey

Stream: new members

[Isak Colboubrani]

As a beginner in Lean and a maths undergraduate, I'm curious about individual learning paths for mastering Lean.

1. How and when did you discover Lean?
2. What was your path to learning Lean, and which resources did you find helpful?
3. If you were starting from scratch in 2024, what learning path would you choose?

[Gareth Ma]

1. February 2023
2. I picked a Maths theorem (in number theory IIRC) and proved it. I think I read MIL a bit, but funny enough I found reading the Mathlib source code more useful... Then I repeat
3. The same

[Damiano Testa]

Gareth, you took my Lean module that started in October 2023: do you want to revise your answer to 1?

[Kevin Buzzard]

The best way to learn lean is to do a project.

[Gareth Ma]

Damiano Testa said:

Gareth, you took my Lean module that started in October 2023: do you want to revise your answer to 1?

Sorry, I meant February 2023... :tear: :tear: :tear: :tear:

[Gareth Ma]

I agree with Kevin though. I guess I will plug my repo https://github.com/grhkm21/lean/ which documents my journey (literally). My first project was trying to prove Mersenne primes and the Euclid-Euler Theorem
Replace lean with lean4 for Lean 4