Projects

Stream: ItaLean 2025

[Rémy Degenne]

Will there be time in the program for participants to work on formalization group projects during ItaLean?
I'm asking because I saw #maths > Ring of integers in quadratic fields, in which Riccardo Brasca is thinking about a possible project for that workshop.
If yes, then I'll prepare some project topics as well.

[Pietro Monticone]

Yes, we’ll be sharing with you all the tentative schedule very soon.

[Pietro Monticone]

Relevant announcement #announce > ItaLean 2025: Bridging Formal Mathematics and AI @ 💬

[Oliver Butterley]

Thanks @Pietro Monticone , @Lorenzo Luccioli and the others for all your work organizing this event! Looking forward to being there.

I was wondering how the "project work" sessions are organized. A couple of us are interested in software verification and keen to connect to anyone else interested in such. Is it compatible with the event if a few of us spend some of the project work slots on this project in a loose and self-organized way?

[Pietro Monticone]

Hi @Oliver Butterley, thank you for your interest in taking part in the event.

All participants will receive an email with all the details regarding the project work session in a few hours.

Yes, the project work session will be very flexible, so you are welcome to devote some of the project work slots to this project in a loose and self-organised way.

[Oliver Butterley]

Great! Thanks for the clarifications.

See you soon! Unfortunately I won't arrive until Wednesday lunchtime because of teaching commitments.

[Lorenzo Luccioli]

Hi everyone,

Following up on the email sent a moment ago, here are the main details about how project work at ItaLean will be organized.

Project proposals

We invite participants to start proposing projects in the shared Google Sheet and to discuss them in this thread.

A project proposal only needs three things:

• a project name

• a short description

• the name of a proponent

After that, others (including the proponent) can volunteer to be informal or formal managers, or simply express interest in participating.
Roles

• The informal manager is someone who knows the mathematics behind the project or feels confident navigating that area. They help clarify the goals and explain the theory when needed.

• The formal manager is someone comfortable with Lean who can help set up the repository, guide the formalization choices, and coordinate the proof development.

Expressing interest

Adding your name under a project means you are potentially interested in working on it during the project sessions. You can express interest in several projects, though as a guideline we suggest not exceeding three or four. In the end we expect each participant to choose one project to focus on.

Presentations on day 1

During the project management session on Tuesday, the organizers will select a set of projects to be presented briefly (about two to three minutes each). Selection will depend on having volunteers for both informal and formal roles, and on the level of interest in the project. After these presentations, participants will choose the project they will join.

Project scope

A project can be a small standalone task or a well defined part of a larger ongoing project, but it should be something where a small group can reasonably make progress during the allocated project work sessions.

Final presentations

On the last day, each active project will be invited to give a short informal update on what was achieved and what the next steps might be. No written report is required.

Feel free to add proposals and comments here in the thread, but don't forget to update the Google Sheet. Looking forward to seeing the ideas that emerge!

[Juanjo Madrigal]

Hi :wave:

I've been looking into Mathlib and it seems that there is currently no development of de Rham Cohomology, although many of the needed tools to define it are already there. Would this be a good topic for a project?

There has also been some discussion in the past about it, so perhaps it is already done somewhere or not the kind of content needed for Mathlib right now.

[Riccardo Brasca]

The usual question is de Rham cohomology of what? Differential manifold? Algebraic varieties? In my opinion it's a little too ambitious for a project for beginners, in the sense that getting to something that really works is not easy. On the other hand if someone just want to try they will surely learn a lot even if at the end the definition is not really "mathlib ready".

[Riccardo Brasca]

Concerning the algebraic theory the state of the art is surely #18551

[Juanjo Madrigal]

I was thinking in cohomology of smooth manifolds, and yes, it's a big topic. I'm not sure if it is useful to start implementing some definitions / results that help in further work, or if it is better to only start projects that can be fully finished during the conference

[Riccardo Brasca]

It is surely OK to work on projects not doable in one week, but writing definitions is often the most difficult part of the formalization. But again, writing a definition and then realizing that it is impossible to compute any concrete example is not a waist of time, it's the way we learn how to write the good one!

[Filippo A. E. Nuccio]

Juanjo Madrigal said:

I was thinking in cohomology of smooth manifolds, and yes, it's a big topic. I'm not sure if it is useful to start implementing some definitions / results that help in further work, or if it is better to only start projects that can be fully finished during the conference

Be aware btw the the differential geometry library tries to abstract as much as possible and to treat Ck manifolds and smooth ones on an equal footing.

[Bhavik Mehta]

This isn't an area I know well, but #mathlib4 > Milestone: B_{dR} seems like something worth being aware of on this point

[Kevin Buzzard]

That relates to the algebraic theory again I guess

[Michael Rothgang]

Juanjo Madrigal said:

I was thinking in cohomology of smooth manifolds, and yes, it's a big topic. I'm not sure if it is useful to start implementing some definitions / results that help in further work, or if it is better to only start projects that can be fully finished during the conference

Hi! I'm glad you're interesting in formalising a differential geometry topic. There is a lot left to do, so helping hands in this area are always welcome :-)

That said, I'm not sure if this project is a good choice. It is being actively worked on (so your work will repeat what others are doing) --- and that work is happening in a separate repository, not mathlib. Also, differential forms in mathlib are not a beginner-friendly topic. You would be setting yourself up for quite a challenge! If you really, really, really want to work on this, you should talk to @Yury G. Kudryashov about the current state of the project, and base your work on their repository.

[Michael Rothgang]

If you care about improving mathlib, I would rather pick a different project. Two ideas coming to my mind are

• defining oriented manifolds: you could build on previous work, but that work was never quite complete --- help making it complete would be a very nice addition.
• given a smooth manifold with a proper action of a discrete group, define the manifold structure on the quotient. (Then you can e.g. define real projective space as a smooth manifold.)

Both are much more doable than something about differential forms.

[Michael Rothgang]

For additional ideas, which will likely take much longer, see e.g. my messages at #new members > Looking for Differential Geometry Project @ 💬 or #new members > Looking for Differential Geometry Project @ 💬

[Kevin Buzzard]

For beginners it's much easier to prove theorems than make more definitions. It's also very hard nowadays for beginners to contribute to mathlib.

[Chris Henson]

There was some recent discussion about reduction systems, essentially theorems regarding relations that have properties such as confluence, the diamond property, etc. This is a bit on the border of math and computer science, but it might be nice in a one-week project setting because it doesn't require too much machinery to get started. @Cody Roux formalized a bit of Term Rewriting and All That a while back, but to my knowledge there has not been much more work on this area.

[Michael Rothgang]

Kevin Buzzard said:

For beginners it's much easier to prove theorems than make more definitions. It's also very hard nowadays for beginners to contribute to mathlib.

Note that the degree of difficulty depends very much on the field of mathematics: in differential geometry, there is (or will be soon) a bunch of low-hanging fruit - in turn, differential geometry is not an easy area to formalise in.

[Juanjo Madrigal]

Thank you for your comments! @Michael Rothgang I'll definitely look into it after the conference :raised_hands:

[Bhavik Mehta]

Chris Henson said:

There was some recent discussion about reduction systems, essentially theorems regarding relations that have properties such as confluence, the diamond property, etc. This is a bit on the border of math and computer science, but it might be nice in a one-week project setting because it doesn't require too much machinery to get started. Cody Roux formalized a bit of Term Rewriting and All That a while back, but to my knowledge there has not been much more work on this area.

I formalised enough of the parallel confluence section of the book to get to confluence of SKI, in case that helps

[Chris Henson]

Bhavik Mehta said:

I formalised enough of the parallel confluence section of the book to get to confluence of SKI, in case that helps

Yes, this could be a useful reference if people are interested in working on this.

[Yoichi Hirai]

I proved something about finite directed graphs two weeks ago in Lean ("there's a path from source to sink when source has net-outflow and ..."). The formalization is not meshed into Mathlib, so I'd like to figure out the next steps.

My impression is that the symmetric Mathlib.Combinatorics.SimpleGraphis much richer than the directed Mathlib.Combinatorics.Digraph. I guess there's opportunity to add paths, cycles, cycle spaces, and things in https://www.epfl.ch/labs/disopt/wp-content/uploads/2018/09/chapter06.pdf for instance.

[Yoichi Hirai]

(Chapter 6 of Game‐Theoretic Foundations for Probability and Finance looks formal enough. I don't have a compelling reason for this non-standard treatment, but in case anyone has interest.)

[Bhavik Mehta]

Chris Henson said:

Bhavik Mehta said:

I formalised enough of the parallel confluence section of the book to get to confluence of SKI, in case that helps

Yes, this could be a useful reference if people are interested in working on this.

https://gist.github.com/b-mehta/e412c837818223b8f16ca0b4aa19b166
I think a formal version of TRaaT would be amazing to have

[Bhavik Mehta]

I have added another project to the sheet, but I'd also like to mention here that I'm happy to help out the formal parts of projects involving software verification, in particular using the Std.Do framework.

[Jannis Limperg]

I just had this idea, so haven't thought it through, but there should still be a lot of basic lemmas in Mathlib that are missing grind/Aesop annotations. I'd be happy to set up a project to work on this. It's beginner-friendly in the sense that you get to learn about parts of Mathlib without wrangling Lean too much, and it should be immediately useful to Mathlib. But of course it's not the typical Mathlib work that people probably want to learn about. For a more ambitious angle, we could also look for opportunities to automate with custom tactics where the standard tactics don't quite do the job. Anyone interested in this?

[Rémy Degenne]

The project idea(s) I wrote in the form is about stochastic processes in continuous time, but I'd be happy to help anyone who wants to do a project related to probability, statistics, or machine learning theory.

Another idea I had, which would be nice to have in Mathlib: Ville's inequality on the supremum of a discrete time nonnegative supermartingale. It's probably too short for a week-long project, but we might discover that we are missing other lemmas and it could be fine.

[Jannis Limperg]

Added the automation project to the doc. Leo will give us a practical intro to grind as well. :)

[Hang Lu Su]

Hi everyone, :hi:

I am a beginner with Lean and mathlib4, and I just completed my PhD degree in geometric group theory. One project that interests me is making incremental progress towards a formalization of the Reidemeister–Schreier method in group theory. (I wrote an introductory chapter about this in my thesis p. 169-177, attached.)
thesis.pdf

From a quick look at mathlib4, it seems that the theorem itself is not yet there, although some related results are the definition of a Schreier transversal, the Schreier lemma, and the PresentedGroup infrastructure. I may very well be missing things, so please correct me if this impression is inaccurate.

Because I am a beginner, I do not have a good sense of how realistic it would be for a (potential) small group of beginners to make useful progress on this this week.

In particular, I am not sure how far along is the support of mathlib4 for finitely presented groups, and if it would be more useful to work on that?

I am happy to adjust my plans if my idea is too ambitious or simply not a good fit, so suggestions of alternative but related projects are very welcome.

[Kevin Buzzard]

I was very surprised to find last week that although Lean had finitely-generated groups and finitely-presented algebras, it did not seem to have finitely-presented groups. docs#PresentedGroup is an explicit construction of a group from a set (or as we say here, a type) of generators and a set of relations, docs#Group.FG is a predicate on groups saying "I am finitely-generated" and docs#Subgroup.FG is a predicate on subgroups of a group saying they're finitely generated, but we don't seem to have Group.FinitelyPresented or Subgroup.FinitelyPresented (and perhaps the former is more use than the latter; I'm not sure). I think that this would be a great beginner project; ideally you would consult with experts on how to state the theorems you want to prove, and then try and prove them yourselves. The step from set theory to type theory is a bit subtle here: in Lean groups and subgroups are different things -- in set theory a subgroup "is" a group but in Lean a subgroup can be turned into a group, but a subgroup is a term and a group is a type, which means that sometimes there can be several ways of translating statements from paper mathematics into Lean and you want to do the translation in such a way as to make the proofs as straightforward as possible rather than having to wrestle with foundations.

[Hang Lu Su]

Thanks! I'm definitely interested in working on something like that. I'll look into the documents you provided and hopefully pick up enough at the workshops to get started tomorrow.

[Chris Henson]

Jannis Limperg said:

I just had this idea, so haven't thought it through, but there should still be a lot of basic lemmas in Mathlib that are missing grind/Aesop annotations. I'd be happy to set up a project to work on this. It's beginner-friendly in the sense that you get to learn about parts of Mathlib without wrangling Lean too much, and it should be immediately useful to Mathlib. But of course it's not the typical Mathlib work that people probably want to learn about. For a more ambitious angle, we could also look for opportunities to automate with custom tactics where the standard tactics don't quite do the job. Anyone interested in this?

Please also feel free to look at CSLib as part of this if you'd like. We make extensive use of grind, but there are some improvements to be made, as we have a fairly long list of exceptions to #grind_lint in this test. This could be an opportunity to try out the new constraint feature of grind_pattern. In particular the System F formalization there has a concentration of performance issues currently.

[Chris Henson]

Also, I have added an entry for term rewriting to the projects spreadsheet.

[Farruh Habibullaev]

Hi everyone! I’m very new to Lean, Mathlib, and mathematical formalization (I’ve only done some basic theorem proving so far). I’m thinking about starting a small project for the event to add some foundational lemmas to Mathlib on finite sets, cardinalities, and injective/surjective functions.

These results are elementary but widely used, and from my searches, it seems that some versions are either missing or not presented in a clean, unified way. Examples include:

• strict subset ⇒ strictly smaller cardinality
• cardinality after removing elements
• injective endomaps on finite types being bijective
• cardinality decomposition lemmas
• existence of maxima on finite sets

It seems like a good beginner-friendly project, but I might be misunderstanding what already exists. Would this be considered a meaningful project, or are these lemmas already present in Mathlib in forms I’ve overlooked?

[Lawrence Wu (llllvvuu)]

docs#Finset.card_lt_card
docs#Finset.card_erase_lt_of_mem
docs#Finite.injective_iff_bijective
docs#Finset.card_union
docs#Finset.max'

[Bhavik Mehta]

I would say that all of these are in mathlib already, but you're certainly not the first to find them tricky to identify!

[Farruh Habibullaev]

Thank you both for your response, Lawrence and Bhavik. I appreciate it. What do you think about proving Hamiltonian paths in tournament graphs? At least proving one classical theorem that every finite tournament contains a Hamiltonian path, a path visiting every vertex exactly once in the correct direction. However, if I understand it correctly, the graph theory in Lean primarily focuses on the undirected graphs.

[Yongxi Lin (Aaron)]

I see that many interesting projects are happening in ItaLean. Is it possible for someone like me — who unfortunately couldn’t attend ItaLean — to participate in these projects online?

[Lorenzo Luccioli]

The plan for this afternoon’s project session is to transfer to the math department (the address is Piazza di Porta San Donato 5). We will split in two rooms:

• Laboratorio Levi (first floor), follow @Lorenzo Luccioli

  • Brownian Motion
  • Quadratic Integers
  • Kolmogorov Complexity
  • Lp Spaces
  • Sphere Packing
  • Improve Automation
  • Optimal Transport
  • Finitely Presented Groups

• Aula Arzelà (fifth floor), follow @Giovanni Paolini and @Pietro Monticone

  • Erdos 337
  • Sum of Three Squares
  • Quotient Manifolds
  • Formal Conjectures
  • q,t-Catalan
  • Finite Subgroups of F(2, F)
  • Term Rewriting
  • Spherical Harmonics
  • Reintroduction to Proofs

[Lawrence Wu (llllvvuu)]

Is there wi-fi on the first floor?

[Lorenzo Luccioli]

The wi-fi is only with eduroam, unfortunately we have no way to set up another wi-fi network for today.