Math AI Lab University of Washington
Spring 2023

Spring 2023 Projects

All projects
theorem mgf_of_iid
{Y : ℕ → Ω → ℝ}
{Z : ℕ → Ω → ℝ}
(h_meas : ∀ (i : ℕ), Measurable (Y i))
(h_indep : ProbabilityTheory.iIndepFun (fun (i : ℕ) => inferInstance) Y μ)
(hident : ∀ (i j : ℕ), ProbabilityTheory.IdentDistrib (Y i) (Y j) μ μ)
(Z_def : ∀ n : ℕ, Z n = (Real.sqrt n)⁻¹ • (∑ i ∈ Finset.range n, Y i)) :
  ∀ n : ℕ, n > 0 →
    ∀ t : ℝ, mgf (Z n) μ t = (mgf (Y 0) μ ((√n)⁻¹ * t)) ^ n := by
  intro n hn t
  rw [Z_def]
  rw [ProbabilityTheory.mgf_smul_left]
Source: uw-math-ai/central_limit_theorem, CentralLimitTheorem/main.lean
  • 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

Projects:

  • Lagrange's Theorem (Dhruv Ashok):
    • If G is a finite group and H ⊆ G is a subgroup, then the order of H divides the order of G.

  • Abstract term rewriting (Gregory Baimetov):
    • The confluence and the Church-Rosser property are equivalent (see Wikepidia).
    • Formalize the principle of well-founded induction (see Wikepidia).

  • Simplicial homology / tactics (Zachary Banken):
    • 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 → V are linear transformations such that the range of S is contained in the nullspace of T, then (ST)² = 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 → X is a contraction mapping, then T has a unique fixed point.

  • Euclidean Geometry (Rico Qi and Edward Yu):
    • 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):
    • 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).