Zulip Chat Archive

Stream: new members

Topic: Contributing to mathlib4 as a beginner

Andreas Gittis (Oct 07 2023 at 01:36):

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 (Oct 07 2023 at 04:57):

@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 (Oct 07 2023 at 09:16):

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

Andreas Gittis (Oct 07 2023 at 16:23):

@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 (Oct 07 2023 at 19:52):

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.


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

Andreas Gittis (Oct 08 2023 at 04:19):

@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.

Last updated: Dec 20 2023 at 11:08 UTC