Contributing to mathlib4 as a beginner

Stream: new members

[Andreas Gittis]

Hello everyone. So I've crunched my way through TPIL and most of MIL, and I'd like to start contributing to mathlib4. It seems to me that there are two options: (i) join a team of people who are already working on a formalizing project (ii) start my own fresh project.

The advantages to (i) are that it would be probably be a more accessible way to get familiar with the process, and I imagine I would mostly be filling in sorry statements and not organizing theory and writing definitions. I feel fairly confident that when I complete a proof it will follow the mathlib4 style guide and create minimal work for editors. The disadvantage is it might not exist - at least when I took a look at the help-wanted tags I didn't see much in the way of organized projects.

My concern with (ii) is that I'm not confident in my ability to create definitions that have good style, correctly reflect the statement I'm trying to formalize, and are compatible with mathlib4 conventions. When I see the definition of an object that is already familiar to me, I am able to get a functional knowledge of how to use it in Lean, but I cannot imagine having created the definition as it exists in mathlib. I don't want to volunteer help only to offshore the bulk of the work to some editor who has to correct my definitions.

I wanted to ask the following questions: For (i), are there groups like this currently operating? If so, is there a way to get a list of the topics being worked on? For (ii), what can I do to ensure I have good definitions/theory structure? Should I post in the mathlib4 zulip, can I submit files that have only statements and sorry's for review before I start proving things? Also would appreciate any general advice people have, given my limited perspective. Thanks.

[Johan Commelin]

@Andreas Gittis Welcome! There are several on-going projects, but it depends a lot on your mathematical background whether you can just jump in and start filling in sorrys. Can you tell us a bit more what your mathematical experience/interest is?
For many people, their first contribution to mathlib is just some hobby project that they enjoyed working on. And there are still plenty of gaps... so I think both (i) and (ii) are viable strategies.

[Anatole Dedecker]

I agree with Johann, I think the main deciding factors are your background and what you like to work on

[Andreas Gittis]

@Johan Commelin @Anatole Dedecker Thanks. I guess my background is basically the standard math graduate student coursework. I've since changed fields to computer science so I'm probably a bit rusty, but when I was a math student I passed quals in complex analysis, topology, and algebra and I worked in logic/computability theory. If I could choose I'd do something in computability or algebra. I saw the halting problem in mathlib, but I didn't see Gödel's incompleteness theorems, so if I was doing my own project I'd probably start with those. Otherwise, if I was joining a project which was more advanced than graduate coursework I would likely have to do something in algebra.

[Martin Dvořák]

FYI https://www.cs.ru.nl/~freek/100/ says that Gödel's incompleteness theorem (1st?) has been formalized in Isabelle, HOL Light, and Coq.

https://www.isa-afp.org/entries/Incompleteness.html
https://github.com/coq-community/hydra-battles/tree/master/theories/goedel

I'd have a look at it before doing it in Lean.

[Andreas Gittis]

@Martin Dvořák Okay thanks I'll take a look. I think it will be interesting to compare approaches because I believe Lean has a much larger library of compatible theories to draw from compared to other ITPs.