Math AI Lab University of Washington
Winter 2023

Winter 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: Gregory Baimetov, Zachary Banken, William Dudarov, Griffin Golias, Raymond Guo, Eva Hu, Luca Li, Lawrence Lin, Alex Sanchez
  • Github repository

Projects:

  • Identities of the Fibonacci sequence Fₙ (Lawrence Lin):
    • F₍ₙ₎F₍ₙ₊₂₎-F₍ₙ₊₁₎² = (-1)^(n+1)
    • F₍ₙ₎F₍ₘ₊ₙ₎ = F₍ₙ₊₁₎F₍ₘ₎ + F₍ₙ₎F₍ₘ₋₁₎
    • m | n ⟹ F₍ₘ₎ | F₍ₙ₎
    • Binet's Formula: F₍ₙ₎ = (1/√5)((1+√5)/2)^n - ((1-√5)/2)^n

  • Group theory exercises from Herstein Abstract Algebra (Alex Sanchez):
    • Let G be an abelian group, and let h₁, h₂ ∈ G be elements. Prove that there exists an element h ∈ G whose order is the least common multiple of the orders of h₁ and h₂.
    • Let G be an abelian group, and let H₁, and H₂ be subgroups. Prove that there exists a subgroup of G whose order is the least common multiple of the orders of H₁ and H₂.

  • Topology (Zilu Li):
    • If f : X → Y is a quotient map, then for each y ∈ Y the set f⁻¹({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.