THE NEW FRONTIER
We are witnessing a paradigm shift. When machines reason alongside humans, mathematics becomes infinitely generative—accessible to everyone. Human intuition and AI verification converge. Mathematical discovery enters a new era.
OUR MISSION
Co-founded with Xinze Li and Jiaqi Lai, Infinity Archive is building the future of human-AI collaboration for mathematics and scientific discovery. We believe the future of science is collaborative and verifiable, powered by mathematical superintelligence.
Our vision is to create an ecosystem where researchers, students, and AI systems work together seamlessly— democratizing access to advanced mathematical reasoning, formal verification, and scientific discovery tools.
OPENMATH INITIATIVES
In parallel, I lead the OpenMath Initiatives at Columbia University Software System Lab, Field Institute Center for Mathematical AI, and Risklab International, under the mentorship of Prof. Ronghui Gu. This research focuses on system-level reasoning through AI-assisted formal verification, making advanced mathematics accessible and verifiable for researchers worldwide.
The OpenMath project advances language models that can understand, generate, and verify mathematical proofs, bridging the gap between natural language intuition and formal mathematical rigor.
AI FOR MATHEMATICS
Projects and seminars I follow closely in the field of AI for mathematics.
Organized by Ben Chow (UCSD) and Zilu Ma (UT Knoxville)
Weekly research seminar at Rutgers on Lean and other AI methods
Tesla Zhang's work, a proof assistant I follow closely
Zaiwen Wen's team work at BICMR, PKU
Kevin Lacker's team work, a theorem prover