More Learning Materials?

Stream: general

[Erika Su]

After having finished Theorem Proving in Lean4, Functional Programming in Lean and some part of manual. I still feel extremely insuffiicient for writing proof as neat and useful in mathlib. Are there any materials to go further?

[Shreyas Srinivas]

Erika Su said:

After having finished Theorem Proving in Lean4, Functional Programming in Lean and some part of manual. I still feel extremely insuffiicient for writing proof as neat and useful in mathlib. Are there any materials to go further?

I found the porting exercise to be the best way to learn the innards of lean 4. Trying the natural number game, topology game or Euclidean Geometry Game also felt useful.

For me personally, the reason this works is that being able to write nice proofs often hinges on good definitions and theorem statements, and this is non-trivial to learn when starting from scratch, so working on new projects was tough. When porting files however, the definitions and theorems are already in place. There is already a proof in lean3 to guide the process and understand what is happening. This provides a lot of opportunities for comparing and contrasting what tactics do in lean 3 and lean 4.