Math AI Lab University of Washington
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
Eight accepted papers · ICML 2026

Congratulations to our ICML authors

The UW Math AI Lab celebrates eight papers accepted to ICML 2026 and its workshops. Congratulations to every author and project team represented in Seoul. DiScoFormer was selected for an oral presentation, and Multiplication Beyond Groups received a Spotlight at the Mechanistic Interpretability Workshop.

July 6–11, 2026 COEX · Seoul, Korea
ICML 2026
Math AI Lab members at ICML 2026 at COEX in Seoul
Math AI Lab at ICML 2026 · COEX, Seoul, Korea
Math AI Lab group at ICML 2026 in COEX, Seoul
ICML 2026 group photo
Math AI Lab members in front of the ICML 2026 sign at COEX
ICML 2026 · COEX, Seoul, Korea
Three Math AI Lab members at ICML 2026 at COEX
Math AI Lab members at ICML 2026 · COEX, Seoul, Korea
Five Math AI Lab members at the ICML 2026 display at COEX
Math AI Lab at ICML 2026 · COEX, Seoul, Korea
Accepted work

Eight papers from across the lab

  1. DiScoFormer: Plug-In Density and Score Estimation with Transformers Oral presentation
  2. Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance
  3. Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models
  4. Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization
  5. Multiplication Beyond Groups: Stratified Fourier Mechanisms in Transformer Circuits Spotlight
  6. Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium
  7. Learned Interventions Inside Lean 4's grind
  8. FactorLibrary: From Polynomials to Circuits via Recursive Subgoals
UW 2026 Lean Hackathon banner
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 Sep 7, 2026
Announcement Online

Fall 2026 project leader applications open

Math AI Lab

Project leader applications for Fall 2026 are open! We are recruiting leaders for projects in four areas: machine learning and AI for math, formalization and autoformalization, autoresearch, and AI for math education and learning. Applications are due Monday, September 7 at 11:59 pm, and earlier applications have priority. Mentors of continuing projects are required to fill it out. The project descriptions are linked below.

Project Lead application formProposed Fall 2026 projects