23
$\begingroup$

tl;dr: Are there any good introductions/tutorials on how to formalize definitions and theorem statements in Lean? (in contrast to introductions on formalizing proofs)


Some background: I am a phd student in combinatorial optimization and a few month ago I decided that I wanted to learn more about proof assistants and in particular Lean. So, I set myself the goal to try to get to a point where I can start to formalize mathematics I am actually currently working on (e.g. some exercises or even some lemma from my thesis) - just to have a goal and see whether I like it.

So, I read/worked through some of the "obvious" introductions (like the natural number game and Theorem proving in Lean) and I think I am now at a point where I can formalize some non-trivial proofs. However, whenever I am now trying to work on something new, I notice that I get mostly stuck on writing the definitions/theorem statements and I get the feeling that I don't really know how to do them "the right way" for Lean (e.g. when should I use def/class/structure/instance/...? Should my objects be types or sets? What arguments should should be implicit/explicit? ...?).

Now, I understand that this is probably just another non-trivial thing one has to learn but I don't really know of any resources I can learn this from. Some of the tools get explained in the later chapters of "Theorem proving in Lean", but at least for me there is not enough relating these explanations to their applications in mathematics. One can of course also look into mathlib for examples, but most of the time this just shows me what a good formalization looks like but not really why it is the way it is and how one gets there.

So, in conclusion: Are there any good introductory texts or video tutorials on how write good definitions/theorems in Lean? (or any other ways to learn how to do that)

$\endgroup$
3
  • $\begingroup$ True, videos are helpful as well! I included this now $\endgroup$
    – GraffL
    Feb 11, 2022 at 1:16
  • 2
    $\begingroup$ The course I'm currently teaching is here ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2022 and there's accompanying videos and lots of examples of writing definitions and proving theorems. It will grow until March 2022 (next up is some topology and some number theory). $\endgroup$ Feb 12, 2022 at 16:02
  • $\begingroup$ @KevinBuzzard: Oh, this has grown a lot since I last saw this. So, thanks for reminding me of your course. I will definitely check this out! $\endgroup$
    – GraffL
    Feb 13, 2022 at 23:29

1 Answer 1

18
$\begingroup$

Lean for the Curious Mathematician 2020

You seem to be the exact right audience for this workshop. We have video recordings on youtube: https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

Tutorials

Some other tutorials and resources are listed here: https://leanprover-community.github.io/learn.html#hands-on-approaches

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.