MechMath develops research systems, specialized provers, benchmarks, and formal verification tools for trustworthy mathematical discovery.
A coordinated research environment in which a knowledge-base manager, natural-language prover, and formal-language prover form a closed loop for discovery, proof development, and Lean verification.
Purpose-built systems that focus on particular theorem-proving settings, representations, or mathematical domains.
Euclidean geometry
A Mathlib-native agentic system for faithful autoformalization and certified theorem proving in Euclidean geometry.
Automated theorem proving
A specialized automated theorem-proving system based on formal decomposition and iterative proof refinement.
Open evaluation sets and verified artifacts for measuring progress in mathematical formalization and theorem proving.
Formal geometry
A benchmark and artifact collection for evaluating autoformalization and certified theorem proving in Euclidean geometry.
Reusable proof-engineering tools that connect symbolic computation with kernel-checked formal reasoning.
Lean 4 tactics
Lean 4 tactics for the automated formal verification of Gröbner-basis properties and computations.
MechMath Systems is an evolving research program. New systems and capabilities will be introduced here as they become available.
