AI for the development and use of mathematics.
We track tools and ideas that accelerate both formal mathematical research and the applied mathematics that drives scientific progress. Below are the broad themes; individual projects and papers are being ported here gradually — for now, the full portfolio lives on our creator's research page.
Formal Proof Assistants
Lean, mathlib, theorem proving, proof search, tactic generation, and library-scale formalization of mathematical knowledge.
Mathematical Discovery
Conjecture generation, analogy, symbolic computation, automated lemma discovery, and proof planning.
Scientific Modeling
PDEs, optimization, inverse problems, simulation, conservation laws, uncertainty quantification, and numerical validation.
Learning Systems
Neural models that help translate between informal reasoning, formal proof, code, and experimental evidence.
Notable projects
Bundle Adjustment Solver
Fast, scalable 3D reconstruction solvers using deflation and multigrid methods.
Lean formalization studies
Small, verifiable theorem examples used to prototype AI-assisted proof workflows.
Optimization for scientific computing
Provably fast solvers for large-scale numerical and scientific problems.
For full papers, projects, and publications
The complete research portfolio — publications, ongoing projects, and academic background — is maintained on our creator's personal page, and will be gradually ported into AI Mathematician under these broad themes.