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 Wednesdays 56:30 pm in Communications (CMU) B006. If you are interested in participating, please contact jarod
at uw
dot edu.
Resources for learning lean
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.