Syllabus

Projects and stubs of ideas

Project title	Comments and possible Mathlib reference

Past projects

Click to expand

Project title	Comments and possible Mathlib reference
The Halting Problem	The definition of a Turing machine in Mathlib
Jordan Normal Form	Generalized eigenspaces in Mathlib
Post’s Functional Completeness Theorem	Not in Mathlib
Liouville’s Theorem	Liouville Theorem in Mathlib
Green’s Theorem	Not in Mathlib
The Isomorphism Theorem	Various isomorphism theorems are in this file in Mathlib
Properties of Trees	The definition of a tree in Mathlib
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.

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
• Define one of the 26 sporadic finte simple groups and prove some of its properties
• 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

• Counterexamples in Topology,
• Counterexamples in Analysis.

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!

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.

---

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

Back to Moodle

This site is open source. Improve this page.