The flagship mathematics programme at Crab Research. Proof Engine develops reliable AI-assisted mathematical research through precise statements, readable arguments, and reproducible proof evidence.
Programme by Alex Chengyu LiCombinatorics · Number theory · Geometry38 mathematical results · 6 methodology papers
Mathematical results 38
A reading route through open problems, classifications and constructive theories.
A formalization writes a theorem and its proof in a form that a proof assistant can check.
Which coefficient sequences come from symmetric tropical matrices? A constructive criterion connects realization, reconstruction and parameterized algorithms.
Working Paper · SSRNFull formalization not yet availableFirst public
Selections introduce different contributions; review levels remain specific to each paper.
Trust and verification standards
Formal verification expresses a theorem and its proof in a form a proof assistant can check. The categories below explain which checks are complete and which assumptions remain.
Internally reviewed manuscript (Paper Close)
Paper Close marks a working paper prepared and internally reviewed before release. Please treat it as an ordinary scholarly preprint: further checking or discussion may lead to corrections. It does not indicate complete formal verification or external peer review.
Machine verification using cited theorems (Reference-Gated)
The code takes the statements of documented cited theorems as inputs and checks the subsequent deduction. The cited theorems' proofs are outside the current verification package; Reference-Gated describes this coverage boundary.
Verification from foundational axioms only (Kernel-Only)
The proof assistant checks every theorem dependency, including cited results, without additional theorem assumptions. Only foundational axioms, the starting principles listed here, are allowed. We also check correspondence to the paper; exposition may still need correction.
Accepted by a journal or peer-reviewed proceedings after independent review. This records external scholarly acceptance; acceptance and formal publication are recorded separately.
Kernel-Only is our only accepted final formalization standard. Reference-Gated has lower assurance and is released only as an intermediate milestone when the engineering effort is exceptionally large. Peer review does not remove a remaining theorem assumption.
These standards describe the evidence for a mathematical claim. Novelty, attribution and correspondence to the original question require separate review; errors discovered after release require correction or withdrawal. Release and correction commitments
Read the verification methods and limits
Exact theorem dependencies
Cited results must have precise statements, sources and corresponding checked formal theorems. Existing kernel-checked Lean/mathlib proofs may be reused. All dependencies must ultimately reduce to propext, Classical.choice and Quot.sound; extra theorem axioms, sorry and unchecked native-computation shortcuts are excluded.
A Reference-Gated release must publish its gate manifest: exact statements, hypotheses and quantifiers, source locations, formal assumptions and the conclusions that depend on them. Reaching Kernel-Only requires eliminating every gate through checked proofs and rechecking the final endpoint and paper correspondence.
The endpoint axiom report identifies what the proof actually depends on. Its statement must still be checked against the intended mathematical theorem; an axiom report alone does not establish that correspondence.
We believe AI-assisted mathematics makes an explicit engineering layer increasingly important: connecting candidate arguments to checked, readable and maintainable results. The Proof Engine programme explores two interacting roles: reliable mathematical production, and structural research that interprets results, develops concepts and opens new directions. These roles can overlap, and AI can assist both; specialist mathematicians remain central to deeper structural understanding. Public problems provide starting points for reusable mathematical contributions. The programme is assessed through the results it supports, the evidence for their claims, their subsequent use and the correction of errors. Read our research programme.
Methodology
Proof Engine 1.0 and 2.0
Proof Engine is a research programme for reliable AI-assisted mathematics. Its two published methodological frameworks are complementary: 1.0 organizes proof development; 2.0 governs the investigation and can use 1.0 within it. Read the programme and its commitments
Proof Engine 1.0
Proof development
Composes exact claims, evidence and dependencies; keeps proof obligations explicit and propagates corrections through the argument.
Governs the question, intended contribution and evidence needed for a mathematical investigation. Autonomous execution remains within human-approved scope.
SSRN Working Papers present developed research. Some are maintained as standalone working papers by design. Research maturity and publication status are recorded separately.
6 papers · First public: newest first · Records updated 2026-10-11
A research programme for reliable AI-assisted mathematics, specifying release and correction commitments, accountable authorship, and interacting roles in mathematical production and structural research.
Theorem Notary lets projects reuse a theorem through its exact statement while keeping its complete proof, definitions, dependencies and foundational axioms open to inspection and checking. This is its Glass Box design. Certificates bind these materials; signatures identify suppliers, and projects preserve valid checks as they derive and publish further results.
A complementary project-level method for source inquiry, existing-solution checks, statement correspondence, and the governance of changing mathematical objectives.
Companion case study in the Proof Engine programme: worked Hamilton and Rado audits of claim-level evidence, checking boundaries and residual dependencies. The flagship Proof Engine Infrastructure paper develops the general methodology.
