eXperimental Lean Lab (XLL)
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.
We are currently meeting on Mondays 11:301 in CLK 120. 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
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
 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 formpreserving map \(g: U \to U'\) where \(U, U' \subset V\) are subspaces. Then there is a formpreserving 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 ConroyTaggart: 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 ChurchRosser property are equivalent (see wikipedia).
 Goal: Formalize the principle of wellfounded 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 nonempty 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 \(n1\) 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_{m1} \)
 \(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.