🧮 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.
ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings (2025)
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.
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.