Conan Xu
AI4Math · Optimization · Formal Mathematics
I work on AI4Math, optimization, and formal mathematics, and build tools for research and learning.
A simple question connects my projects: how can a mathematical idea become something we can understand, compute, and verify? I study the convergence and failure of ADMM iterations, formalize optimization algorithms in Lean 4, and explore how AI can participate in mathematical research.
I also keep a blog for derivations, project notes, and ideas that become clearer as I learn.
Selected research
All researchAI-assisted discovery of counterexamples for three-block ADMM
Direct three-block ADMM can fail even when its third constraint block is the identity. Periodic orbits expose the limits of this structure and provide a case study in AI-assisted mathematical discovery.
Adaptive ADMM in Lean
Formalizing convergence analysis for adaptive ADMM in Lean 4, making the connections between algorithms, parameter strategies, and mathematical assumptions explicit.
Research software
All projectsVeryMath Course Copilot
A study workspace that keeps textbooks, questions, explanations, and learning materials together.