The challenge
Research-level mathematics demands both creative leaps and unforgiving rigor. Bridging informal arguments and machine-checkable proof, at scale, is an open problem.
AIProver is a unified neuro-symbolic framework for translating informal mathematics into Lean 4, supporting working mathematicians, and enabling novel discovery.
Research-level mathematics demands both creative leaps and unforgiving rigor. Bridging informal arguments and machine-checkable proof, at scale, is an open problem.
An auto-formalizing LLM, with Semantically-Aligned Models (SAMs) to enrich the context window with definitions, produces candidate Lean proofs; SAT/SMT solvers, computer algebra systems, and tactic-level metaprogramming verify and repair them in a tight feedback loop.
An ever-expanding, self-improving knowledge base of verified mathematics, and a credible path to attacking long-standing open problems in group theory, analysis, and beyond.
Core research thrusts driving AIProver toward scalable, verified mathematical reasoning.
Translating informal mathematics into Lean 4, then synthesizing and repairing proofs through tight loops between LLMs, SAT/SMT solvers, computer algebra systems, and tactic-level metaprogramming.
An interactive, conversational aide for working mathematicians, capable of answering technical questions, suggesting relevant lemmas, sketching proof strategies, and grounding every suggestion in formally verified knowledge.
Training Semantic Alignment Models (SAMs) that align informal and formal proofs in a shared embedding space, enabling RAG retrieval, concept search across fields, and hierarchical proof refinement, foundational to ProofBridge.
Attacking open problems on simplicity and structure of infinite groups, including those tied to infinite-dimensional Lie algebras and P. M. Neumann's open problem (F21), via G-Simple and GAP integration.
Verifying inequalities and asymptotic estimates with O-Forge, and formalizing the OEIS at scale through Sequencelib.