The AIProver toolchain

A domain-specific solver for group theory and abstract algebra. G-Simple integrates with GAP (Groups, Algorithms and Programming) to attack open problems on simplicity, perfectness, and structure of infinite groups, including those arising from infinite-dimensional Lie algebras.

A project to formalize the mathematics of the On-Line Encyclopedia of Integer Sequences in Lean 4, targeting over 100,000 sequences and tens of millions of theorems about their values. Led by Walter Moreira with Joe Stubbs.

An LLM and computer algebra framework for verifying inequalities and reasoning about asymptotic behavior. O-Forge complements general-purpose provers with techniques tailored to the structure of analytic estimates, developed by Ayush Khaitan and Vijay Ganesh.

A reasoning module for quantified formulas, statements with "for all" and "there exists" that sit at the heart of mathematical logic. AI-QFT pairs learned heuristics with SAT/SMT solvers to tackle quantifier-rich problems.