Syllabus
Projects and stubs of ideas
| Project title | Comments and possible Mathlib reference |
|---|---|
| Properties of Trees | The definition of a tree in Mathlib |
| The Isomorphism Theorem | Various isomorphism theorems are in this file |
| Green’s Theorem | I don’t think that this is in Mathlib |
| Liouville’s Theorem | Liouville Theorem in Mathlib |
| Post’s Functional Completeness Theorem | I don’t think that this is in Mathlib |
| Jordan Normal Form | Generalized eigenspaces |
| The Halting Problem | The definition of a Turing machine in Mathlib |
Past projects
Click to expand
| Project title | Comments and possible Mathlib reference |
|---|---|
| Cauchy’s Theorem (Complex Analysis) | Cauchy’s Integral Formula in Mathlib |
| Sylow’s Theorems | Sylow’s Theorems in Mathlib Most of the file Sylow is relevant. |
| Perfect Graphs | Perfect graphs and examples. There is a folder Mathlib/Combinatorics/SimpleGraph/, but I do not think that perfect graphs are in Mathlib. |
| Lusin’s Theorem | |
| Ostrowski’s Theorem | Ostrowski’s Theorem. As far as I can tell, it is not in Mathlib, but there are some (possible) formalizations. Relevant Zulip chats:Link to LLL and Ostrowski’s Theorem thread |
| A Special Case of Dirichlet’s Theorem on Arithmetic Progression | Special case of Dirichlet’s Theorem on arithmetic progressions. |
| Fermat’s Little Theorem | Fermat’s Little Theorem in Mathlib. Euler’s Theorem in Mathlib |
| Lagrange’s Theorem | Lagrange’s Theorem in Mathlib |
| Sieve Theory | Some results in analytic number theory. |
| Combinatorial Problems | Problems taken or inspired by IMO problems. |
Orphaned projects
-
Hall subgroups and their existence in soluble groups
I could not find Hall’s theorem in Mathlib, the file on Sylow’s Theorems is relevant.
- Cap set problem
- Cantor’s Theorem
- Group cohomology
- Transcendence of π
- Ramsey Theory
- Probability theory and game theory
- Matrix analysis and QR decompositions
- The Basel problem in Mathlib
- For material on sums of two squares, look at SumTwoSquares.
Mathematically oriented projects
- Sums of squares of a field are a group with zero
- The non-zero sums of squares of a field form a multiplicative group
- Derivatives of polynomials are continuous
- In a semiring, 0 is odd if and only if 2 has a multiplicative inverse and 1 has an additive opposite
- Characterise semirings in which 1 is even
- Sums and products of continuous functions are continuous
- Polynomials over an integral domain are an integral domain
- Irrational numbers exist
- Find infinite subsets of the natural numbers containing no 3-term arithmetic progression
- Your favourite theorem!
External repositories and books for inspiration
The .pdfs in Keith Conrad’s blurbs page contain plenty of ideas.
Besides using Lean to prove theorems, you can also use it to verify counterexamples! Two books that contain lots of inspiration are
Computer science oriented projects
- Automating proofs:
- write a tactic to dispatch “junk values”
- write a tactic to compute degrees of multivariate polynomials
- write a tactic to split and progress on
Nat.sub
- Tooling for statistical analysis of Mathlib:
- proof lengths (extract the number of lines of the proofs of all declarations)
- tactic in a declaration (find which tactics are used in a given declaration)
- tactic usage (frequency distribution of tactics)
- finishing tactics (frequency distribution of the last tactic in a proof)
- Come up with your meta-programming goal!
For instructions on how to create a project depending on Mathlib, look at this page.
For browsing the documentation for Mathlib, go to the excellent documentation pages.
Back to the Theorem Proving with Lean webpage
Back to the Mathlib project for the module
