Math AI Lab University of Washington
Fall 2023

Fall 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
  • Falculty 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, …].
    • Members: Xinyan Li, Leopold Mayer, Christie Yang
    • GitHub code

  • Witt's Cancellation Theorem
    • Thm: Let ⟨-,-⟩ be a symmetric bilinear form (i.e. ⟨x,y⟩ = ⟨y,x⟩ for all x,y ∈ V). Suppose that there is form-preserving map g: U → U' where U, U' ⊂ V are subspaces. Then there is a form-preserving map f: V → V extending g.
    • Cor: U ⊕ V ≅ W ⊕ V ⟹ U ≅ 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(# 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.
    • Members: Zhongrui An, Hermann Chau, Vasily Ilin, George King, Benjamin Li, Yu He Zhang
    • GitHub code

  • Formalizing Math 300
    • Goals:
      • 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
    • Members: Yanzhe (Steven) Zhong, Anthony Xing, Luca Li, Chengyu (Kenneth) Gong
    • GitHub code