1.0/Proof development
Claims, evidence and dependencies
Construct, verify and connect mathematical results.Crab Research brings together Proof Engine, a mathematics research programme, and independent work in computer science and the social sciences.
Mathematics research programme
Proof Engine develops reliable AI-assisted mathematics through mathematical results, public methodology and formal verification: writing theorems and proofs in a form a proof assistant can check.

Claims, evidence and dependencies
Construct, verify and connect mathematical results.Questions, contributions and changing objectives
Steer inquiry, track contributions and adapt direction.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.
An infinite lattice path answers Erdős’s question; the theorem also prescribes almost every limiting direction in an interval.
Explore this resultWhich coefficient sequences come from symmetric tropical matrices? A constructive criterion connects realization, reconstruction and parameterized algorithms.
Explore this resultReference-Gated proofs check the deductions while assuming explicitly listed cited theorems whose proofs are not included in the package.
Working Paper · Zenodo
Working Paper · Zenodo
Working Paper · SSRN
Outside the mathematics programme
Papers outside Proof Engine, organized by research field.
Algorithms, machine learning, AI evaluation, and technical systems.
Browse papers