🧮 AI for Mathematics
This page highlights ongoing and past research efforts connecting AI, formal methods, and mathematical reasoning at the reasoning and learning research group @ Georgia Tech led by Professor Vijay Ganesh.
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness (2026)
Authors: Prithwish Jana1, Viet Bach Hoang1, Logan Luna1, Viresh Pati2, Akash Singirikonda1, Cy Xie3, Lisa Carbone4, Wuyang Chen5, Walter Moreira6, Joe Stubbs6, Sriram Vishwanath1, Vijay Ganesh1
Affiliations: 1Georgia Institute of Technology, USA | 2University of Pennsylvania, USA | 3Foothill College, USA | 4Rutgers University, USA | 5Simon Fraser University, Canada | 6University of Texas at Austin, USA
TL;DR: AIProver is an open-weight Lean agent that post-trains a 119B language model while evolving its agentic harness via certificate-driven search (HarnessEvolve), using a semantic alignment model and symbolic verifiers as rewards. On research-level mathematics it lifts semantic correctness from 15.7% to 36.7% standalone, and to 79.8% as a Claude Code skill.
Semantic Alignment Models: A Bridge Between Informal and Formal Mathematics (2026)
Authors: Prithwish Jana1, Sriram Vishwanath1, Vijay Ganesh1
Affiliations: 1Georgia Institute of Technology, USA
TL;DR: Semantic Alignment Models (SAMs) are joint embedding models, trained by semantic contrastive learning, that map semantically equivalent informal (natural language) and formal (Lean 4) mathematics to a shared representation space. Instantiated as ProofBridge, SAMs improve cross-modal retrieval by up to 3.28× over a strong text encoder and boost downstream proof auto-formalization by +31.14% semantic correctness and +1.64% type correctness.
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings (2026)
Authors: Prithwish Jana1, Kaan Kale1, Ahmet Ege Tanriverdi2, Cruise Song1, Sriram Vishwanath1, Vijay Ganesh1
Affiliations: 1Georgia Institute of Technology, USA | 2Bogazici University, Turkiye
TL;DR: ProofBridge is a unified framework that translates natural language theorems and proofs into Lean 4 using joint embeddings, cross-modal retrieval-augmented fine-tuning, and iterative proof repair, achieving strong semantic and type correctness gains.
Sequencelib: A Platform for Formalizing Sequences from The On-Line Encyclopedia of Integer Sequences (OEIS) (2025)
Authors: Walter Moreira1, Joe Stubbs1, Vijay Ganesh2
Affiliations: 1TACC, University of Texas at Austin, USA | 2Georgia Institute of Technology, USA
TL;DR: Sequencelib is a formal library in Lean 4 that encodes thousands of integer sequences from the OEIS catalog and millions of theorems about them, along with metaprogramming tools to index sequences, compute values, and relate equivalent sequences.
O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis (2025)
Authors: Ayush Khaitan1, Vijay Ganesh2
Affiliations: 1Rutgers University, USA | 2Georgia Institute of Technology, USA
TL;DR: An LLM-CAS framework to quickly obtain full proofs of asymptotic estimates that are commonly and laboriously calculated in research mathematics.
MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (2016)
Authors: Curtis Bright1, Albert Heinle1, Ilias Kotsireas2, Saeed Nejati1, Krzysztof Czarnecki1, Vijay Ganesh1
Affiliations: 1University of Waterloo, Canada | 2Wilfred Laurier University, Canada
TL;DR: MathCheck applies Boolean satisfiability (SAT) solvers and computer algebra systems (CASs) to efficiently search for mathematical objects and automatically generate computer-assisted proofs of combinatorial conjectures. It often solves problems thousands of times faster than either a SAT solver or a CAS.