UW's eXperimental Lean Lab (XLL) is a subsidiary of the Washington Experimental Mathematics Lab (WXML). The XLL provides a space for mathematicians at any level (faculty, postdocs, PhD students, undergraduates, high school students, ...) to learn about formalizing mathematics with Lean and to collaborate with others on projects.

If you are interested in participating, please contact jarod at uw dot edu.

Resources for learning lean

• Play the Natural Number Game (by Kevin Buzzard and Mohammad Pedramfar).
• Install a Lean 4 environment on your computer with VS Code: follow the directions here.
• Our main source this quarter will the Avigad and Massot's interactive book Mathematics in Lean.
  • Follow the instructions in Section 1.1 "Getting Started" to download the "mathematics_in_lean" repository which you should be able to view in VS Code.
• Our secondary source will be Buzzard's 2023 course Formalizing Mathematics.
• Join the Lean community Zulip.
• Additional resources
  • Mathlib documentation.
  • List of math courses using Lean maintained by the Lean Community.
  • Watch Kevin Buzzard solve exercises on his youtube channel.
  • Browse the resources on the Lean community
  • Browse resources on the Lean website.
  • Avigad, de Moura, and Kong's book Theorem Proving in Lean
  • Read Kevin Buzzard's blog Xena project.

Winter 2024

• Faculty mentors: Jarod Alper, Andy Heald
• Graduate student mentors: Herman Chau, Vasily Ilin, Leopold Mayer
• Student participants: Dale Dai, Yujia Dai, Siyuan Ge, Tess Gerrard, Kenneth Gong Daniel Hughes Mitchell Levy Benjamin Li, Xinyan Li, Nathan Louie, Rina Reimer, Alexander Sanchez, Qiguang Yan, Christie Yang, Steven Zhong
• Projects:
  • FRACTRAN
    • Implement the programming language FRACTRAN in Lean and write the adder in FRACTRAN.
    • Members: Vasilly Ilin, Alex Sanchez, Mitchell Levy
    • github code
  • Continued Fraction Expansion for \(e\) (continued from Fall 2023)
    • The continued fraction expansion of \(e\) is \([1, 0, 1, 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8, 1, 1, 10, \ldots]\).
    • Members: Xinyan Li, Leopold Mayer, Christie Yang
    • github code
  • Witt's Cancellation Theorem (continuation from Fall 2023)
    • Thm: Let \(\langle-,-\rangle\) be a symmetric blinear form (i.e. \(\langle x,y \rangle = \langle y,x \rangle\) for all \(x,y \in V\) ). Suppose that there is form-preserving map \(g: U \to U'\) where \(U, U' \subset V\) are subspaces. Then there is a form-preserving map \(f: V \to V\) extending \(g\)
    • Cor: \(U \oplus V \cong W \oplus V \implies U \cong W\).
    • Members: Andy Heald, Nathan Louie, Sarah Mathison, Qiguang Yan
  • Formalizing Math 300 (continuation from Fall 2023)
    • Goal: Formalize the exercises (and possibly results) in the Math 300 textbook by Conroy--Taggart: An Introduction to Mathematical Reasoning.
    • Write a Lean guide for students taking Math 300
    • github code
    • Members: Chengyu (Kenneth) Gong, Rina Reimer, Tess Gerrard, Anthony Xing, Yanzhe (Steven) Zhong,

Fall 2023

• Faculty mentors: Jarod Alper, Andy Heald, James Morrow
• Graduate student mentors: Herman Chau, Vasily Ilin, Leopold Mayer
• Undergraduate TA: Zilu (Luca) Li
• Student participants: Anthony Xing, Benjamin Li, Chengyu Gong, Christie Yang, George King, Nathan Louie, Qiguang Yan, Sarah Mathison, Xinyan Li, Yanzhe (Steven) Zhong, Yu He Zhang, Zhongrui An
• Projects:
  • Continued Fraction Expansion for \(e\)
    • The continued fraction expansion of \(e\) is \([1, 0, 1, 1, 2, 1, 1, 4, 1, 1, 6, 1, 1, 8, 1, 1, 10, \ldots]\).
    • Members: Xinyan Li, Leopold Mayer, Christie Yang
    • github code
  • Witt's Cancellation Theorem
    • Thm: Let \(\langle-,-\rangle\) be a symmetric blinear form (i.e. \(\langle x,y \rangle = \langle y,x \rangle\) for all \(x,y \in V\) ). Suppose that there is form-preserving map \(g: U \to U'\) where \(U, U' \subset V\) are subspaces. Then there is a form-preserving map \(f: V \to V\) extending \(g\)
    • Cor: \(U \oplus V \cong W \oplus V \implies U \cong W\).
    • Members: Andy Heald, Nathan Louie, Sarah Mathison, Qiguang Yan
  • Random Graphs
    • Goal: Build a random graph \(G(n,p)\) with \(n = \#\) of nodes with \(p =\) probability of an edge. Show that the expected number \(E(\# \text{edges in } G(n,p))\) of edges in a random graph \(G(n,p)\) is \({n \choose 2} p\). Related goals: compute other expected numbers, e.g. number of triangles in a random graph.
    • github code
    • Members: Zhongrui An, Hermann Chau, Vasily Ilin, George King, Benjamin Li, Yu He Zhang
  • Formalizing Math 300
    • Goal: Formalize the exercises (and possibly results) in the Math 300 textbook by Conroy--Taggart: An Introduction to Mathematical Reasoning.
    • Write a Lean guide for students taking Math 300
    • github code
    • Members: Yanzhe (Steven) Zhong, Anthony Xing, Luca Li, Chengyu (Kenneth) Gong

Spring 2023

• Faculty mentor: Jarod Alper
• Graduate student mentors: Vasily Ilin, Leopold Mayer
• Student participants: Dhruv Ashok, Gregory Baimetov, Zachary Banken, Dianna E., Luca Li, Lawrence Lin, Rico Qi, Timothy Tran, Alfie Xu, Edward Yu
• Github repository: vilin97
• Projects:
  • Lagrange's Theorem (Dhruv Ashok)
    • If \(G\) is a finite group and \(H \subseteq G\) is a subgroup, then the order of \(H\) divides the order of \(G.\)
  • Abstract term rewriting (Gregory Baimetov)
    • Goal: The confluence and the Church-Rosser property are equivalent (see wikipedia).
    • Goal: Formalize the principle of well-founded induction (see wikipedia).
  • Simplicial homology / tactics (Zachary Banken)
    • Goal: Formalize simplicial homology including definitions of simplicial complexes, faces, and the chain group as well that the square of the boundary operator is zero.
    • Functional programming and writing simple tactics in Lean.
  • Linear algebra (Dianna E.)
    • If \(V\) is a vector space and \(S, T: V \to V\) are linear transformations such that the range of \(S\) is contained in the nullspace of \(T\), then \( (ST)^2 = 0. \)
  • Compactness (Luca Li)
    • If \(X\) is a compact space, then every closed subset is also compact.
    • If \((X,d)\) is a metric space and every infinite subset of \(X\) has a cluster point, then \(X\) is sequentially compact.
  • Banach Fixed Point Theorem (Lawrence Lin)
    • If \((X,d)\) is a non-empty complete metric space and \(T: X \to X\) is a contraction mapping, then \(T\) has a unique fixed point.
  • Euclidean Geometry (Rico Qi and Edward Yu)
    • Goal: formalize Euclidean Geometry based on Hilbert's Axioms by defining points, lines, angles, and the notion of distance.
    • Formalize a solution to Problem 1 on USAMO 2023.
  • Graph theory (Timothy Tran)
    • Goal: Every tree on \(n\) vertices has \(n-1\) edges.
  • Mean Value Theorem (Alfie Xu)
    • Formalize the Mean Value Theorem (currently relying on Rolle's Theorem).

Winter 2023

• Faculty mentor: Jarod Alper
• Graduate student mentors: Vasily Ilin, Leopold Mayer
• Student participants: Gregory Baimetov, Zachary Banken, William Dudarov, Griffin Golias, Raymond Guo, Eva Hu, Luca Li, Lawrence Lin, Alex Sanchez
• Github repository: vilin97
• Projects:
  • Identities of the Fibonacci sequence \(F_n\) (Lawrence Lin)
    • \( F_n F_{n+2}-F_{n+1}^2=(-1)^{n+1} \)
    • \( F_n F_{m+n}=F_{n+1}F_m+ F_n F_{m-1} \)
    • \(m | n \implies F_m | F_n\)
    • Binet's Formula \(F_n = \frac{1}{\sqrt{5}} \big( (\frac{1+\sqrt{5}}{2})^n - (\frac{1-\sqrt{5}}{2})^n \big) \)
  • Group theory exercises from Herstein Abstract Algebra (Alex Sanchez)
    • Let \(G\) be an abelian group, and let \(h_1, h_2 \in G\) be elements. Prove that there exists an element \(h \in G\) whose order is the least common multiple of the orders of \(h_1\) and \(h_2\).
    • Let \(G\) be an abelian group, and let \(H_1\), and \(H_2\) be subgroups. Prove that there exists a subgroup of \(G\) whose order is the least common multiple of the orders of \(H_1\) and \(H_2\).
  • Topology (Zilu Li)
    • If \(f : X \to Y \) is a quotient map, then for each \(y \in Y\) the set \(f^{-1}(\{y\}) \) is connected. If \(Y\) is connected, then so is \(X\).
    • If a set is connected, then so is its closure.
    • In a metric space \( (X,d) \), the following are equivalent: (a)\(X\) is compact, (b) Every infinite subset of \(X\) has a cluster point, (c) Every sequence in \(X\) has a convergent subsequence, (d) \(X\) is complete and totally bounded, (e) \(X\) is totally bounded and has the Lebesgue property.
  • Commutative algebra (Raymond Guo)
    • An integral domain is a PID if and only if every prime ideal is principal.
  • Sequences (Zachary Banken, Gregory Baimetov)
    • Beatty's Theorem (aka Rayleigh's Theorem): see wikipedia.
    • Uspensky's Theorem: it is not possible to partition the natural numbers using 3 or more Beatty sequences.

Fall 2022

• Faculty mentor: Jarod Alper
• Graduate student mentors: Vasily Ilin, Leopold Mayer
• Student participants: Zachary Banken, Griffin Golias, Raymond Guo, Eva Hu, Hastin Kapoor, Luca Li, Lawrence Lin, Alex Sanchez
• Github repositories: raymondpg vilin97
• Project: Formalizing solutions to exercises from undergraduate math textbooks such as Axler's book Linear Algebra Done Right, Mukres's book Topology; a first course, Silverman's book A Friendly Introduction to Number Theory, Silverman and Tate's book Rational Points on Elliptic Curves, Folland's book Advanced Calculus, Rudin's book Principles of Mathematical Analysis, and Hungerford's book Abstract Algebra: An Introduction.

Spring 2022

• Formalizing Hilbert's Basis Theorem
  • Faculty mentor: Jarod Alper
  • Graduate student mentors: Vasily Ilin, Leopold Mayer
  • Student participants and contributors: Griffin Golias, Kevin Kuei, Brendan Murphy, Alex Scheffelin, Runchi Tan
  • Project: Developed our own library for ideals of commutative rings and formalized Hilbert's 1890 proof that ideals in polynomial rings are finitely generated.
    • github