Ideas for a reading course on learning Lean

Stream: new members

[Jérémie Turcotte]

Hi everyone! I'm a PhD student at McGill University studying mostly graph theory. This fall a friend and I want to learn Lean, and make it a reading course (since we only have 1 course left, our supervisors have approved this idea). There appears to be a lot of ressources for learning Lean (I've just finished the Natural Number Game for instance). I'm wondering what you would suggest is a reasonable objective for a 1 semester (self-taught) course on mathematics with Lean would be? Would you say that after a semester we should be at a level to be able to either contribute to the community somehow and/or be able to use Lean at a research level? If so, do you have any recommendations of what we should do? (In particular, I have to suggest a course contents description to the university to create this reading course.) I've seen the Learning Lean page (with links to various tutorials and books), and I know there is also Prof. Buzzard's "Formalising Mathematics" course from last fall on GitHub. Thanks!

[Yaël Dillies]

Hey! What kind of graph theory are you interested in?

[Jérémie Turcotte]

I've worked mostly on graph searching (so games like Cops and Robbers, Graph burning, etc.), and minor-free stuff (Hadwiger-type results), but am interested in other graph theory questions as well. For Lean specifically, I would love to eventually work on graph theory stuff in it, but for learning I am happy with any context (in fact the friend I plan to start learning with is not in graph theory).

[Kevin Buzzard]

I would do a project rather than just attempting to do some generic "learning". People learn Lean very well by doing.

[Violeta Hernández]

Yeah, I read through most of the Lean book but most of it went over my head until I actually tried working with Lean

[Kevin Buzzard]

So if you're happy to go down that route then the question becomes what project to do and that would be easier to answer if we knew what your friend was interested in. Of course you could work on a project each. I would figure that out first and then dress up the project as a course, cite examples of books like #tpil or a lean paper or two and say you're going to read these and then make a project on top, say you'll use this chat instance for support. Then just find something in graph theory or whatever which isn't in mathlib and work on it. I don't know enough about the subject to know what would be an appropriate project in graph theory but I do know that as of a few months ago all the key basic definitions are in place.

[Kevin Buzzard]

How about stating the Hadwiger conjecture and proving it for small n like n=1 or n=2? I'm being serious. This will be harder than it sounds because you'll have to decide how to do minors. Stuff which is pictorially completely trivial like "if you contract this edge and then throw away that one, it's the same as throwing away that one and then contracting this one" might be really messy if you choose a bad definition. Definitions are hard, proving theorems about definitions which are already there with a good API is much easier.

[Vincent Beffara]

Here https://github.com/vbeffara/lean/tree/main/src/graph_theory is one option for defining minors, contractions and such things (based on push-forwards of simple_graph terms, e.g. a contraction of a graph is defined as essentially a push-forward with connected cosets). That is enough to show that minor_of is transitive, which indeed was harder to show than I thought, exactly for this kind of reasons that commuting edge deletion and edge contraction is not so trivial.

[Jérémie Turcotte]

Thanks a lot for your suggestion! Your time answering me is really appreciated! I definitely think we'll go in this direction of doing a project.

[Frédéric Dupuis]

Defining expander graphs and proving basic results about them might be another good project idea.