Student projects

I have been involved in the supervision of several undergraduate Lean projects since 2017. Here are some examples.

Kenny Lau — formalisation of the statements of the local Langlands conjectures for abelian algebraic groups. First year undergraduate project 2018. Won the pure project prize. GitHub. Kenny formalised a lot of the structures necessary to state the local Langlands correspondence for tori.

Chris Hughes — formalisation of proofs of Sylow’s Theorems. First year undergraduate project 2018. Github. Chris proved all of Sylow’s theorems in Lean, and his proof of Sylow 1 is now in mathlib.

Ali Sever — Euclidean geomety in Lean. Summer project 2018. GitHub. Ali formalises Tarski’s version of Euclidean geometry.

Ramon F. Mir — Schemes in Lean. MEnd project 2019. Won the JMC maths project prize. Github. Ramon gave a definition of schemes in Lean; his ideas were incorporated in mathlib recently.

Anca Ciobanu — Group Cohomology in Lean. BEng project 2019. pdf and GitHub. Anca defined H^0 and H^1, and proved the long exact sequence of terms of low degree in group cohomology.

Lambert A’Campo and Ashvni Narayanan — compact unit ball implies finite-dimensional. LSGNT computing project 2019. GitHub. Lambert and Ashvni prove that if a normed vector space over a nondiscrete complete normed field has compact unit ball then it is finite-dimensional.

Shenyang Wu — Group Cohomology in Lean. MSci project 2020. GitHub. Shenyang defined H^n for all n. Here is his write-up.

Ellen Art — Dots and boxes in Lean. MSci project 2020. GitHub. Ellen develops the theory of the man in the middle in Lean.

Xiang Li — Eudoxus’ construction of the reals. Xena summer project 2020. Github. Xiang develops the theory of reals as equivalence classes of “almost linear” functions from the integers to itself.

Harun Khan — Squares in the Fibonacci sequence. Xena summer project 2020. Github. Harun formalised Cohn’s proof that 144 is the largest square in the Fibonacci sequence.

Jamie Bell — a statement of the Birch and Swinnerton-Dyer conjecture. LSGNT student mini-project 2021. Github. Jamie formalised a statement of the BSD conjecture. He did not prove all intermediate results along the way (for example he did not prove that the L-function of an elliptic curve has a holomorphic extension to a neighbourhood of s=1, because this is a profound theorem), but he defined all the data, and sorried various theorems.

Other projects

The Leanprover-community website also has a list of projects which use Lean or mathlib.