How much lean is necessary for Mathlib?

Stream: new members

[Stephen Zhou]

Hi everyone,
I've been learning lean by (slowly) reading through Mathematics in Lean. I've already finished the natural number game. What I'm curious about is how much Lean I actually need to know to understand/contribute to Mathlib. There seems to be a scary amount of type theory behind it, and I don't think I actually understand any of it. So how much type theory (and just other lean stuff) do you need to know to get Mathlib?

[David Ledvinka]

If you also know the area of math you plan to contribute to well I think this is enough (in particular if you could do most of the exercises in MIL). You don't need to know type theory (although a little bit of "naive" type theory can help)

[David Ledvinka]

I would also say it requires more type theory and lean knowledge to come up with proper definitions than to prove theorems, so for first contributions I think it would be easier to prove something which doesn't require new definitions.

[Lawrence Wu (llllvvuu)]

there is no set prerequisite that applies to all of mathlib in my opinion.

i think type theory is actually much less relevant than “tricks of the trade” like searching, IDE usage, and usage of tactics / commands for experimenting / debugging. but you don’t need to be particularly deft to start contributing. if you work on an area that exists in mathlib you can look at the surrounding code and learn from it. see also https://leanprover-community.github.io/contribute/index.html

[Kevin Buzzard]

FWIW I read #tpil (which is not at all scary and indeed taught me what little type theory I know) and that's about all the type theory I know, it's certainly enough to get you proving theorems. You don't have to know any serious type theory to use mathlib, just like you don't have to know any serious set theory to prove theorems on paper

[Shreyas Srinivas]

I think if you want to progress to metaprogramming, it helps to understand #fpil

Otherwise you don’t need very deep foundational knowledge. It helps to know what a typeclass is and why lean is getting stuck with inferring meta variables when you are debugging your proofs and such. But usually #fpil and #tpil will teach you enough. Nothing replaces the process of learning by doing, getting stuck on errors and asking around or debugging.

[Kevin Buzzard]

You can contribute to mathlib and prove theorems in lean without having the first clue about metaprogramming. Metaprogramming is what you need to know to write tactics. You don't need to know any metaprogramming if all you want to do is use them.

[Arthur Paulino]

Kevin Buzzard said:

You don't need to know any metaprogramming if all you want to do is use them.

I largely agree. I don't fully agree because, just like in regular software engineering, any API can be abstracted to the extent of its documentation and to how faithfully it matches the implementation (accounting for bugs, TODOs etc).

The norm for mathlib tactics is well-written documentation and decent test coverage. But hiccups may still occur, in which case knowing some metaprogramming may help. Or just ask here on Zulip.