Calendar

Events

Agenda and archive for Math AI Seminar activity at UW. Calendar data lives in the repo so new entries are one-object updates.

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

Hosted by Math AI Lab

UW 2026 Lean Hackathon

We hosted the Lean Hackathon as a focused gathering for Lean, formalized mathematics, and AI-assisted mathematics at the University of Washington.

Hackathon site

Mon Jul 6, 2026

Conference 9:00 AM-5:00 PM COEX Convention & Exhibition Center, Seoul, South Korea

ICML 2026

Math AI Lab

Congratulations to the authors of the 7 papers from Math AI Lab projects, which got accepted by ICML 2026 Conference and Workshops!

Does My Embedding Reflect That A=B? Evaluating Mathematical Equivalence in Embedding Models
Learned Interventions Inside Lean 4's grind
Semi-Autonomous Formalization of the Vlasov–Maxwell–Landau Equilibrium
Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
Multiplication Beyond Groups: Stratified Fourier Mechanisms in Transformer Circuits
FactorLibrary: From Polynomials to Circuits via Recursive Subgoals

ICML 2026