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:30-1 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 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.