List of good undergraduate projects

Stream: general

[Vasily Ilin]

Hi.
I will be teaching (the third iteration) of the math formalization class at the University of Washington in Spring 2026. I would like to suggest some projects to the students taking the course. I am aware of https://leanprover-community.github.io/undergrad_todo.html. Are there any other lists of good undergrad formalization projects? Perhaps some there is already a Zulip thread about it (I could not find one)?

[Vasilii Nesterov]

I taught a course on Lean last Spring, and made a list of possible projects that could be added to Mathlib (maybe some of them are already done):

Analysis

• L’Hôpital’s rule for the ∞/∞ case (the 0/0 case is already done)
• Taylor series with the remainder term in Peano and integral forms (Lagrange and Cauchy forms are already there)
• Lemmas about convex functions — e.g. that a differentiable convex function is continuously differentiable
• A continuous nowhere differentiable function: you can either construct a concrete example, or prove that in fact nowhere differentiable functions are dense in the space of continuous functions
• Tikhonov’s theorem: let K be a nonempty compact set in a normed space. Then any continuous function K → K has a fixed point

Topology

• Fundamental groups of spheres: you can start by showing that π₁(Sⁿ) is trivial for n > 1. It can be done ad hoc, but it’s better to proceed by proving the Van Kampen theorem along the way.

Linear Algebra

• Sylvester’s criterion

Group Theory

• Group presentations: Mathlib has a PresentedGroup structure, but no concrete examples yet. For example, you could formalize the presentation of the permutation group (or others from here.

Computability

• Show that the problem “is x = 1 in a given semigroup defined by generators and relations?” is undecidable.
• Computational complexity: this area is in an early stage in Mathlib. Currently, only the class P is defined. You could define NP and provide an example of an NP-hard problem (even a trivial one — or try the Cook–Levin theorem).

Number Theory

• Hurwitz’s theorem (ProofWiki link) on approximating irrational numbers by rationals.

Combinatorics

• Schur’s theorem: for any coloring of the natural numbers in finitely many colors, there exists a monochromatic triple x, y, z such that x + y = z.

Geometry

• Cartan–Dieudonné theorem: every isometry of ℝⁿ can be represented as a composition of at most n reflections.

Measure Theory

• Luzin’s theorem: a function f is measurable on [0, 1] if and only if for every ε > 0, there exists a compact set of measure greater than 1 − ε on which f is continuous.

Complex Analysis

• Gauss–Lucas theorem: the roots of the derivative of a polynomial lie in the convex hull of the roots of the polynomial itself.

---

There is also https://1000-plus.github.io/all

[Kevin Buzzard]

I'm not at all sure that the list you link to (the undergrad todo list) is a list of good undergrad formalization projects; there is a good reason that many of the things on that list are still on that list, and typically that it's because for some reason they make very bad undergrad formalization projects.

[Aaron Liu]

Vasilii Nesterov said:

• L’Hôpital’s rule for the ∞/∞ case (the 0/0 case is already done)

This one is tricky since if you just go to the statement of the 0/0 case and replace 0 by ∞ the resulting statement you get is actually false

[Michael Rothgang]

For @Floris van Doorn's Lean course, we made a list of useful formalisation topics last year: https://github.com/fpvandoorn/LeanCourse24/blob/master/LeanCourse/Project/README.md#formalization-topics
In the next months, we'll make an updated list for this year.

[Vasily Ilin]

@Michael Rothgang , this is very useful, thank you!

[Mirek Olšák]

Speaking of teaching Lean, I am planning the same, so I prepared a preliminary fancy poster. Feel free to edit the SVG to your purposes :slight_smile: .

[Moritz Doll]

Kevin Buzzard said:

I'm not at all sure that the list you link to (the undergrad todo list) is a list of good undergrad formalization projects; there is a good reason that many of the things on that list are still on that list, and typically that it's because for some reason they make very bad undergrad formalization projects.

To expand on this: the l'Hopital rule was formalized by Anatole Dedecker, who is very competent at both maths and Lean and he told me that it was not easy. Similarly, I formalized Taylor's theorem and while getting a first version to work, the mathlib-ready version had quite a lot of revisions (and it is still not ideal).
In the past I used the github issues to write down some low-hanging fruit for contributions to mathlib. I am not sure whether this is still done and whether people are looking there? Maybe we need something on the website to guide people starting out to a list of easy problems.

[Moritz Firsching]

https://github.com/google-deepmind/formal-conjectures tries to have a low entry barrier, and might be suitable when looking for a first small real formalization project: #Formal conjectures > Good first issues links to a list of good first issues and questions about it can be discussed in this channel: #Formal conjectures

[Joseph Tooby-Smith]

There is a list of projects for PhysLean here:
https://physlean.com/ProjectIdeas
And lots of other TODOs which are at undergraduate level.

[Shreyas Srinivas]

Spectral graph theory might be worth a shot. There are lots of graph theoretic properties that can be derived from operations on the laplacian matrix or adjacency matrix

[Shreyas Srinivas]

Actually here is something more concrete:

1. Formalise Cheeger's inequality for undirected graphs

[Shreyas Srinivas]

2. (if this hasn't already been proved elsewhere) : Prove the sherman morrison formula for computing inverses of low rank matrices.

[Shreyas Srinivas]

3. Prove the Mulmuley-Vazirani-Vazirani theorem that lets you randomly pick a minimal element from a set with high probability

[Shreyas Srinivas]

4. Prove Pinsker's inequality for relating different entropy distance measures.

[Bhavik Mehta]

Shreyas Srinivas said:

2. (if this hasn't already been proved elsewhere) : Prove the sherman morrison formula for computing inverses of low rank matrices.

This one has a generalisation in mathlib: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Invertible.html#Matrix.invOf_add_mul_mul. It may be reasonable to add this special case for discoverability though, and using vecMulVec and similar

[Shreyas Srinivas]

5. Here's one more, and I think this is more interesting mathematically than computationally : write the mathematician's version of the ellispoid method with queries to a separation oracle and prove that it finds a feasible point for linear constraints in poly(n,m, log (U)) many queries. Then use the doubling/bisection method to find the right (optimum) value for a linear objective such that you still get a feasible point.

[Shreyas Srinivas]

@Martin Dvořák already has a formalisation of the basic definitions of LPs which can be re-used

[Shreyas Srinivas]

6. Might be calculational : Prove concentration inequalities for probability theory (I am primarily interested in the discrete versions with finitely many random variables).

[Shreyas Srinivas]

One addendum to spectral graph theory : See if you can establish all these relations in slide 7 (starting at page 26 of the pdf) : https://adga-workshop.org/2025/tijn.pdf

[Shreyas Srinivas]

Realistically I expect that proving even a few of these would be decent work for a course project.

[Bhavik Mehta]

A student of mine proved some of the relationships and non-relationships (but not all) between vertex expansion, edge expansion and spectral expansion of directed multigraphs over the summer; I agree there's still lots of scope for spectral graph theory

[Martin Dvořák]

Shreyas Srinivas said:

Martin Dvořák already has a formalisation of the basic definitions of LPs which can be re-used

Indeed. I have a definition of LP and a proof of the strong duality theorem.
Standard LP is here: https://github.com/madvorak/duality/blob/main/Duality/LinearProgrammingB.lean
I might provide a different LP definition if needed.

[Rado Kirov]

I have enjoyed working through Tao's Real Analysis companion - https://github.com/teorth/analysis see #Analysis I (I am working through the book, and at chapter 6, AFAIKT noone has completed all exercises) and have started toying with taking popular math textbooks and writing similar companions for them (https://github.com/rkirov/category-theory-in-context-lean/tree/main/CategoryTheoryInContextLean only so far).

While it doesn't have the thrill of being the first to formalize a deep result (a lot of the results in intro math books are already in mathlib), educationally it can be interesting for students to in a way build a mini-version of mathlib following a well written textbook, learn mathlib much better, do exercises in Lean and pave the way for potentially future math students studying informal and formal math hand-in-hand.

[Michael Rothgang]

Comparing this list with Floris' and mine, let me record that mathlib already has the Gauss-Lucas theorem.

[Michael Rothgang]

And I wonder: do we already have van Kampen's theorem in mathlib? (That name doesn't seem to turn up useful results.)

[Snir Broshi]

Michael Rothgang said:

And I wonder: do we already have van Kampen's theorem in mathlib? (That name doesn't seem to turn up useful results.)

AFAIK we have Van Kampen limits but not the homotopy theorem, although they might be related since the theorem is a statement about limits

[Michael Rothgang]

I also saw those (and didn't check closely how much they are related)