How can I make meaningful contributions with Lean?

Stream: general

[Cameron Rampell]

Hi all,

I'm a high school student who's recently taken up quite an interest in Lean (sorry if I'm not supposed to be making posts like these; I'm new to the Lean Zulip channel). I learned enough to get a part time job over the summer formalizing olympiad problems in Lean4, which wasn't too tricky, and I'm now interested in contributing something larger.

I looked at the list of 100 theorems to formalize in Lean4 and an unformalized result that seemed really interesting was the fact that pi is transcendental. So my friend and I decided to create a blueprint project on what we should do. Earlier today, we found a proof that builds everything from the ground up in a book called Making Transcendence Transparent by Burger and Tubbs and finished formalizing a proof for the irrationality of e; we are currently in the process of proving that e^k, where k is an integer, is irrational.

But I have two concerns with this: one is that we're reinventing the wheel, since it's difficult to see how much has actually been completed here already, and two is that this is too difficult of a project for two high schoolers to actually make progress on. I was really inspired by the proof and research paper about proving Aprey's theorem (i.e. irrationality of zeta(3)) but I'm not really sure what interesting and nontrivial result would be novel to prove in Lean4.

So I'm considering dropping the project before we sink too much time into it – if this is the best course of action to take, please let me know. But I'm still interested in doing something unique with Lean4, so please suggest anything I could help with.

[Ruben Van de Velde]

There's an open pull request that covers that already, I'm afraid. I should probably add a link to it

[Ruben Van de Velde]

The theorems on that list that are accessible to new lean users are all done, I'm afraid

[Ruben Van de Velde]

That is, if you want to contribute to mathlib. If you just want to do a project as a learning experience, that doesn't matter. But in that case, you might want to pick something where you already have a pretty good grasp of the mathematics

[Cameron Rampell]

That's a bummer. Stuff like the four color theorem or Green's theorem seemed way out of reach, so I avoided them; I was also considering formalizing the isoperimetric inequality, but then I realized that also required Green's theorem...

Is there anything about the same difficult as formalizing Aprey's theorem that relatively new lean users could try out? It'd be cool to have a big project like that to work on.

[Chris Henson]

I don't know where you interests lie, but there are also some projects with more applied math/physics/CS flavor. These might be easier to jump in with something more greenfield as you seem to want. Some examples (each of these have channels here) are CSlib, QuantumInfo, and PhysLean. (Not to discourage you at all from contributing to Mathlib, just giving a sampling of what is out there)

[Damiano Testa]

Also, most formalisation projects uncover missing lemmas and library improvements, besides being one of the best ways to learn Lean.

[Michael Rothgang]

In general, I'd recommend becoming clear about what area you want to contribute in (formalisation can be extremely fun, but is also difficult - I highly recommend starting with a piece of mathematics you know really well), and then asking a focused thread about that area. If you'd like, I can try to help you by pinging some relevant people on such a thread.

[Michael Rothgang]

I strongly believe there are good projects in every area, also for your level - but the list of these sometimes sits in the heads of people (and changes over time).

[Michael Rothgang]

Your message sounds like you like elementary number theory. I remember the existence of infinitely many Carmichael numbers being a proposed project a year ago. IIRC @María Inés de Frutos Fernández proposed that: can you update us on the status of that? Do you think this would be an appropriate project here/ can you suggest others? (Thanks a lot. You're a lot closer to number theory than I am!)

[Cameron Rampell]

@Michael Rothgang Yes, I'd say I'm a fan of elementary number theory. Another option may be to formalize some results in Euclidean geometry – my friend and I are both olympiad type people, and I have a bit of experience with that already since I've formalized some (albeit very basic) geometry problems in Lean. But I've been told by people who know far more higher math than I do that Euclidean geometry isn't exactly relevant, and it's also a bit annoying to formalize.

[Cameron Rampell]

Would something like working on formalizing Brun’s Theorem be a way to contribute?

[Kevin Buzzard]

I think you're asking the wrong question, in some sense. It's quite difficult nowadays for someone who's pre-university to contribute to Lean's mathematics library, because pretty much all of the stuff which was accessible to people at undergrad level or below was picked off several years ago. In the 2010s I spent a lot of my time trying to attract mathematics undergraduates into this area, but now I don't do this at all, I focus far more on PhD students, because I ran out of ideas of interesting projects for undergraduates a few years ago, and I'm assuming that you know less than a typical undergraduate at this point. I need people to help me prove Fermat's Last Theorem, and undergraduates are unfortunately typically of no use here because the material is too complex.

I think that the way for someone like you contribute in general, or prepare for mathlib contributions in the future, is to learn more about how the software and the mathematics library works, and the way to do that is to find a theorem (perhaps at a more challenging level than anything you've tried before) for which you understand the underlying mathematics, and just go ahead and try to prove it, and ask here when you get stuck. You'll almost certainly learn something. This way you'll be learning more about the software and will be preparing yourself for meaningful contributions later.

So, for example, I would say: if you understand the proof of Brun's theorem, go right ahead and formalize Brun's theorem! Don't worry about "contributing", concentrate right now on learning.

[Yaël Dillies]

I should add that many people here (including myself) would be very happy to guide you through your first formalisation project so long as the topic bears some relevance to research mathematics

[María Inés de Frutos Fernández]

Michael Rothgang said:

I remember the existence of infinitely many Carmichael numbers being a proposed project a year ago. IIRC @María Inés de Frutos Fernández proposed that: can you update us on the status of that? Do you think this would be an appropriate project here/ can you suggest others?

I proposed a project about Carmichael numbers for last year's formalization course in Bonn (define Carmichael numbers, prove some basic results including Korselt's criterion, and prove that 561 is the smallest Carmichael number).
Some students did this, but as far as I know they never PR'd it to Mathlib.
That being said, I agree with Kevin's point above, I would recommend to start with a project that is interesting to you without worrying about whether it is in the library.

[Michael Stoll]

(Just to chime in on Carmichael numbers: I think formalizing the proof that there are infinitely many is quite hard. IIRC, this involves some heavy asymptotic analysis.)

[María Inés de Frutos Fernández]

(This was not part of the project).

[Riccardo Brasca]

Now that we have quadratic algebras we can compute the ring of integers and the discriminant (someone already mentioned the ring of integers today)

[Kevin Buzzard]

Oh that is a good point! It would be cool to establish the isomorphism between the integers of $\mathbb{Q}(\sqrt{d})$ and the appropriate docs#QuadraticAlgebra , that might well be accessible to Cameron and I could imagine finding a place for it in mathlib. QuadraticAlgebra is new so there's some low-hanging fruit here.

[Timothy Chow]

Is Lindemann-Weierstrass done? I seem to remember that it's in mathlib, but only partially proved. Normally I would consider that to be beyond what high-school students can do, but if Cameron is already working through Burger and Tubbs then maybe it's not out of reach. (By the way, Irrationality and Transcendence in Number Theory by David Angell is another excellent resource for someone trying to teach themselves this topic.)

[Johan Commelin]

It's an open PR

feat: Lindemann-Weierstrass Theorem #28013

[Ruben Van de Velde]

Review of #29121 is welcome

[Kevin Buzzard]

Reviewing PRs containing interesting stuff is definitely making a meaningful contribution :-)

[Arthur Paulino]

Reviewing PRs is also a great way to get to know a new repo, especially in a repo like mathlib with a dynamic chat like this Zulip server. I wouldn't recommend asking beginner questions in the PR itself, but questions are definitely welcome here on Zulip.

"On PR such and such, why did _ do _? What does _ mean?"

[Arthur Paulino]

Some PRs are merged with TODOs. If you spot something you believe you can tackle, why not?

[Arthur Paulino]

Here's a list of issues tagged as good first issue: https://github.com/leanprover-community/mathlib4/issues?q=is%3Aissue%20state%3Aopen%20label%3A%22good%20first%20issue%22

Here's the result of searching "TODO" on the mathlib4 repo: https://github.com/search?q=repo%3Aleanprover-community%2Fmathlib4%20TODO&type=code