First Contribution to Mathlib

Stream: new members

[Aviv Bar-Natan]

Hi everyone! :wave:

I’ve been learning Lean and recently finished the first few chapters of Mathematics in Lean.
As a next step, I’d like to make my first small contribution to mathlib — mainly as a way to learn the workflow and get involved.

I was thinking of starting with a short, elementary combinatorial theorem, for example:

For a set of n distinct natural numbers, the set of all subset sums has at least $\binom{n+1}{2}$ elements.

Before I dive in, I’d like to ask:

1. Does mathlib generally welcome such elementary, self-contained results, or is it focused on more “core” material within each field?

2. For a project at that level, would I likely need to develop a lot of background before I can even state and prove such a result? For example, I have not found the notion of subset-sum of a set. Will I have to first define this object in mathlib?

Thanks a lot for any advice — I’d really appreciate guidance on how to start contributing in a useful way!

[Kenny Lau]

@Aviv Bar-Natan (I don't speak for Mathlib, but)

1. it's a good learning experience to embark on small projects, no matter whether it gets into mathlib or not
2. mathlib aims to prove things in the highest generality; for example, i personally am not a combinatorialist so i'm not very familiar with this, but maybe your argument would work over any AddCommMonoid with cancellative addition?
3. and also, maybe on your way to the result (assuming you actually split into lemmas properly, and not just solve the main goal with 100 lines of code), you might discover some missing steps in the library, some very general lemmas that would help with your project; those small lemmas would be valuable addition to mathlib
4. don't worry about defining subset sum in mathlib, define it yourself first and then we can see what happens
5. please ping me in the process of / after you finish the project, i'm interested to follow up

[Michael Rothgang]

Hi :wave: Welcome to the Lean community; I'm glad you're like to contribute to mathlib!
In general, mathlib likes to build a theory - so proving results that are reusable as much as possible. I am not a combinatorialist, so let somebody else comment if that also applies to the idea you had. Both questions (1) and (2) will have answers depending on the field and project.

What mathematical background do you have? Another option is to ask for interesting good first projects pertaining to your area.

[Michael Rothgang]

So, Kenny answered faster than me - but I guess we are saying very similar things :-)

[Aviv Bar-Natan]

Thank you for your answer!
I’m currently studying for a master’s degree in theoretical computer science, and I’m also taking some math courses on my own to strengthen the background I need for theoretical research.

I really like the idea of asking for a first project! I’m open to any field — I mainly want to go through the contribution process and learn how it works.
I thought about something in elementary combinatorics since it feels the most accessible, but I’d be happy to hear if you have other suggestions.

[Michael Rothgang]

In general, I strongly recommend that you try to formalise a result which you know well. Learning the mathematics and the formalisation at the same time is simply much harder. (So, for instance, while I love new contributions in differential geometry, I wouldn't advise you to pick that unless you're familiar with that area.)

[Snir Broshi]

Hello! :wave:
Aviv Bar-Natan said:

I have not found the notion of subset-sum of a set. Will I have to first define this object in mathlib?

Well there's docs#Finset.sum / docs#Multiset.sum / docs#List.sum which all sum a finite amount of things.
Here's my attempt at a translation of your theorem statement:

import Mathlib

theorem foo_nat (s : Finset ℕ) :
    (s.card + 1).choose 2 ≤ (s.powerset.image (·.sum id)).card := by
  sorry

theorem foo_general {α : Type*} [DecidableEq α] [AddCommMonoid α] (s : Finset α) :
    (s.card + 1).choose 2 ≤ (s.powerset.image (·.sum id)).card := by
  sorry

This takes a finite set of natural numbers, so there are no duplicates.
The LHS is $\binom{n+1}{2}$, and the RHS takes the powerset of the given set, maps each subset to its sum, and finally takes the cardinality of the result.

If you don't need commutativity then you can also work with a List instead of a Finset and require that it has no duplicates with docs#List.Nodup.

In general, searching Mathlib isn't a trivial task, I recommend the following in-order:

• https://loogle.lean-lang.org/
• https://leansearch.net/
• https://deepwiki.com/leanprover-community/mathlib4

but to search on Loogle you have to know some names first, and that's where the other two AIs can help.

[Snir Broshi]

btw how does the proof for this go? I think I saw it or something similar using probabilistic methods, but I'm not sure. I'm also not sure how to formalize probabilistic arguments, but Mathlib does support probability.

[Aviv Bar-Natan]

Thanks that’s really helpful for me. I just tried to formalize the theorem by myself and learned a lot from your generalization to commutative monoid

[Aviv Bar-Natan]

Hi @Kenny Lau , I'm giving you a ping :)
I opened a PR:
https://github.com/leanprover-community/mathlib4/pull/31689

I can share my experience while working on it.
By the way, if you’d like to review my code, I’d really appreciate it!

[Kenny Lau]

@Aviv Bar-Natan I've left some basic remarks there

[Kenny Lau]

I would like those to be addressed first before I move on (ping me when you're done)

[Aviv Bar-Natan]

@Kenny Lau Issues are fixed

[Kenny Lau]

@Aviv Bar-Natan more comments

[Aviv Bar-Natan]

@Kenny Lau Fixed most comments. Wrote some other comments. I'll add a proof that (Finset.range (n + 1)).erase 0 attains the bound.