Winter 2024

Winter 2024 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 mentors: Jarod Alper, Andy Heald
Graduate student mentors: Herman Chau, Vasily Ilin, Leopold Mayer
Student participants: Dale Dai, Yujia Dai, Siyuan Ge, Tess Gerrard, Kenneth Gong, Daniel Hughes, Mitchell Levy, Benjamin Li, Xinyan Li, Nathan Louie, Rina Reimer, Alexander Sanchez, Qiguang Yan, Christie Yang, Steven Zhong

Projects:

FRACTRAN
- Implement the programming language FRACTRAN in Lean and write the adder in FRACTRAN.
- Members: Vasilly Ilin, Alex Sanchez, Mitchell Levy
- GitHub code

Continued Fraction Expansion for e (continued from Fall 2023)
- 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 (continuation from Fall 2023)
- 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

Formalizing Math 300 (continuation from Fall 2023)
- 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
- Members: Chengyu (Kenneth) Gong, Rina Reimer, Tess Gerrard, Anthony Xing, Yanzhe (Steven) Zhong
- GitHub code