AI4Math
Our AI4Math initiative blends formal proof with large‐scale learning:
- Lean Copilot: integrating LLMs to autocomplete tactics and suggest proof steps in Lean.
- Lean Agent: a lifelong learning framework for theorem proving (Kumarappan et al., ICLR 2025).
- Lean Dojo: interactive dashboards for visualizing proof search and tactic performance.
- Lean Progress: first of a kind reward model that predicts how much progress you can make on a Lean proof.
AI4Science
Key neural operator projects from our group:
- Neural Operator: learning mappings between function spaces (Kovachki et al., 2021).
- Fourier Neural Operator: spectral methods for parametric PDEs (Li et al., 2020).
- Physics‑informed NO: embedding physical constraints into operator learning (Li et al., 2021).
- CoDA‑NO: Pretraining codomain attention neural operators for multiphysics PDEs (Rahman et al., NeurIPS 2024).