Neuro-symbolic core
An auto-formalizing LLM proposes; SAT/SMT solvers, computer algebra systems, and Lean 4 verify. Every step is grounded in formal logic.
A collaboration across
An Extensible Neurosymbolic Prover for Mathematical Discovery
A Prover by theorists, for theorists (mathematicians, statisticians, theoretical computer scientists, theoretical physicists, …)
A neuro-symbolic framework pairing auto-formalizing LLMs with SAT/SMT solvers, computer algebra systems, and Lean 4 for proof synthesis, mathematical assistance, and verified discovery.
A collaboration across
A unified pipeline that turns natural-language mathematics into Lean-verified proofs, and acts as a research assistant alongside working mathematicians.
An auto-formalizing LLM proposes; SAT/SMT solvers, computer algebra systems, and Lean 4 verify. Every step is grounded in formal logic.
A conversational research aide for mathematicians: answers questions, suggests lemmas, sketches proof strategies, and grounds suggestions in verified knowledge.
Semantic Alignment Models (SAMs) align informal and formal proofs in a shared embedding space, powering RAG context, concept search, and hierarchical proof refinement.
Tools, libraries, and benchmarks are released openly so the community can verify, extend, and build on every result.
AIProver orchestrates domain-specific tools, each targeting a different mathematical area, alongside the Sequencelib formalization project.