Research
Optimization, formal mathematics, and AI-assisted research.
I study the mathematical properties of optimization algorithms and how AI can help us formulate, explore, and verify mathematical questions. The work below includes a public preprint and ongoing open-source projects.
AI-assisted discovery of counterexamples for three-block ADMM
AI-Assisted Discovery and Construction of a Counterexample to the Convergence of Three-Block ADMM with the Identity Matrix as its Third Constraint Block
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.