Exemplar proofs

Stream: general

[Plam]

I'd like to have a look at some largeish proofs in Lean so that I can get a sense of how such things are done. I'm guessing mathlib is a good place to look. Any particular proofs there that would be instructive to look over? Also I've not looked through that much of the Xena project archives. Are there examples of larger proofs there that I could look at?

[Patrick Massot]

There are different styles of proof, depending on the author but also the intent. Which kind of proof do you want to see?

[Patrick Massot]

There are also different topics of course, are you looking for CS or maths?

[Plam]

CS would be preferable, but I'm happy to look at maths. Could you say more about the styles of proof?

[Patrick Massot]

First you can use direct proof terms, or use tactics, or combine both

[Patrick Massot]

You can aim for a concise proof or a pedagogical proof

[Plam]

I'd prefer to err towards terms rather than tactics. I'm more neutral on pedagogy vs concision, but a slight preference for pedagogy

[Patrick Massot]

Did you have a look at https://github.com/leanprover-community/mathlib/blob/master/src/data/list/basic.lean?

[Patrick Massot]

If you want theoretical CS you can look at https://arxiv.org/abs/1810.08380 and the corresponding code in https://github.com/leanprover-community/mathlib/tree/master/src/computability

[Patrick Massot]

Remember you can download a compiled mathlib at https://github.com/leanprover-community/mathlib-nightly/releases

[Plam]

Hadn't looked at list.basic yet, thanks! And the paper looks excellent

[Kevin Buzzard]

I wouldn't look at the xena project. Most of the stuff there was written by amateurs, in fact most was written by me when I knew very little about how to write Lean code.

[Kevin Buzzard]

In Xena you will see me struggling trying to do basic stuff, and often missing tricks and taking far too long. In mathlib you will see experts writing complex code with very little documentation. My gut feeling is that you want something in between. However it depends on your goals. The reason I am motivated to learn how to write proofs the way the mathlib team write them is so that I can contribute to mathlib. However more recent stuff I've committed to xena is typically attempts to teach undergraduate mathematicians how to write proofs in Lean, and again this might not be what you want. When I was a learner I found data.rat.basic hard going (or data.rat, whatever it's called, I mean the rational numbers). Maybe Patrick's idea is the best -- look at how people built lists from scratch and proved a bunch of basic stuff about them. Many proofs will be short, but the cumulative total is long and some proofs will rely on many many others. I guess in some sense one tries to avoid writing large proofs; one tries to split off as many lemmas as possible.