Internally reviewed manuscript (Paper Close)
Internally reviewed and publicly released. Complete formalization of the principal conclusions is not yet established; errors may remain.
FLAGSHIP PROGRAMME / MATHEMATICS
Proof Engine
The flagship mathematics programme at Crab Research. Proof Engine develops reliable AI-assisted mathematical research through precise statements, readable arguments, and reproducible proof evidence.
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.
Verification with external theorem assumptions (Reference-Gated)
Some cited theorems are stated as explicit assumptions. The proof assistant checks the remaining argument conditional on them; their proofs are not yet included in the released package.
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.
propext (Propositional extensionality); Classical.choice (Classical choice); Quot.sound (Quotient soundness).
Peer-reviewed · accepted
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.
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.
Mathematical results 17
SSRN Working Papers present developed research. Some are maintained as standalone working papers by design. Research maturity and publication status are recorded separately.
17 results · Academic publication first · record updated 2026-09-06
Boolean Antichains in Finite Lattices: Complete Classification, Product Structure, and Matroid Applications
A height-gap classification and product structure for Boolean antichains, with matroid and lattice applications.
Revised 2026-08-31
Ballot-Admissible Fibonacci Ribbon Tableaux: Complete Enumeration for Arbitrary Alphabet Size and Fixed-Rank Asymptotics
Enumeration for every alphabet size, highest-weight refinements, and fixed-rank asymptotics for ballot-admissible Fibonacci ribbon tableaux.
Revised 2026-09-05
Finite-Defect Path Models for Peripheral Benzel Tilings: Propp's Problem 6 and the First Defect Diagonal
Propp’s Problem 6, finite-defect path models, and complete generating functions on the first defect diagonal.
Revised 2026-08-31
Cover Relations and Lagrange Collisions in Rational Dyck Path Orders
Lagrange-value collisions, cover relations, band-fibre structure, and exact minimal examples in rational Dyck path orders.
Revised 2026-09-05
The Exact Extremal Bound in Erdős Problem 848
The exact extremal bound for every N in Erdős Problem 848, including the finite range and infinite tail.
Revised 2026-08-31
Hamilton Cycles and Paths in the Noncrossing Partition Refinement Graph
A complete classification of Hamilton cycles and paths in the noncrossing partition refinement graph, with uniform constructions and parity obstructions.
Revised 2026-08-31
On Rado Numbers for x + by = bz: The b^k Pattern and a Threshold Conjecture
The b^k pattern, finite computational evidence, and a threshold conjecture. This preprint does not claim closure of the full Rado programme.
A Classification-Free Proof of the Root-Polytope Projection Theorem
A uniform, classification-free proof of the known strict factor-two root-polytope projection theorem, with a rootwise bound.
A Permutation Grid with 155 Rook Placements
A permutation grid with exactly 155 complete rook placements, disproving Lewis–Won Conjecture 3.10, with counterexamples in every order at least eight.
An Explicit Collar Recursion for Type-013 Benzel Tilings
An explicit collar construction proves sufficiency for type-013 benzel tileability in Propp’s Problem 4. Full enumeration remains open.
Preliminary Working Papers 7Show papersHide papers
These working papers include early ideas, initial drafts, and work awaiting further development or verification. They are shared as work in progress.
A Two-Corner Decomposition for Fixed Points of 123-Avoiding Permutations
A Catalan-forest decomposition proving the conjectured fixed-point distance formula, with joint position and excedance counts and distance distributions under symmetry.
Infinite paths in the composite-restricted visible lattice
An infinite unit-step path through coprime integer pairs greater than one with a composite coordinate; rays with almost every limiting coordinate ratio in (4/3,5/3).
Reflected Newton Transforms and Concavity of Peak-Polynomial Coefficients
A reflected Newton transform, its symmetric concave image and coefficientwise inequalities, with applications to two peak-polynomial coefficient questions.
Revised 2026-09-03
A constructive inverse theory for symmetric tropical characteristic polynomials
A constructive inverse theory for symmetric tropical characteristic polynomials. The human proof is complete; formalization is in progress.
Repeated-Endpoint Canon Permutations: Cone Walks and Spectral Geometry
The analytic cone-walk companion: probabilistic, harmonic, and spectral geometry. Full formal verification of the paper remains in progress.
Rigidity, Descents, and Wilf Classification in Pattern-Avoiding Canon Permutations
Rigidity, descent formulas, and global Wilf classification for canon permutations. The current public manuscript predates the completed formal package.
A Kernel-Pure Lean 4 Formalization of the Distance Pair Characterization for the Rado Equation x + by = bz
For integers b ≥ 2 and k ≥ 1, the multicolor Rado number R_k(b) for the equation x + by = bz is the least positive integer n such that every k-coloring of {1, ..., n} contains a monochromatic solution.
We believe the significant change in AI-era mathematics goes beyond an increase in output: rapid generation exposes the missing engineering layer connecting verification, interpretation, reuse and maintenance, and opens up a new division of research work. AI can help generate candidate arguments and explore proof paths; emerging roles such as mathematical engineers can turn this material into checkable, reproducible and maintainable results; mathematicians remain central to choosing worthwhile questions, discovering structure, creating concepts, and explaining and generalizing results. These roles can overlap, and Proof Engine is exploring the basic feasibility of this division through public mathematical cases. For the detailed argument, see our methodology paper.
Methodology
Proof Engine 1.0 and 2.0
Complementary layers of mathematical research: 1.0 organizes proof development; 2.0 governs the mathematical investigation and can use 1.0 within it.
Proof Engine 1.0
Proof development
Composes exact claims, evidence and dependencies; keeps proof obligations explicit and propagates corrections through the argument.
Read the paper · SSRN 7237460- First public release
- 2026-07-29
- Latest public revision
- 2026-08-31
Proof Engine 2.0
Research governance
Governs the question, intended contribution and evidence needed for a mathematical investigation. Autonomous execution remains within human-approved scope.
Read the paper · Zenodo Working Paper- First public release
- 2026-09-05
- Latest public revision
- 2026-09-05
Methodology papers 4
SSRN Working Papers present developed research. Some are maintained as standalone working papers by design. Research maturity and publication status are recorded separately.
4 papers · Academic publication first · record updated 2026-09-06
Revised 2026-08-31
Beyond Kernel Verification: The Missing Engineering Layer of Mathematics
A methodological account of statement correspondence, evidence, and the engineering surrounding kernel verification.
Revised 2026-08-31
Proof Engine Infrastructure: A Fail-Closed Claim-Graph Method for Accountable AI-Assisted Mathematical Research
A claim-graph method for accountable AI-assisted mathematical research; the public technical description of Proof Engine 1.0.
Revised 2026-09-06
Claim-Level Verification for AI-Assisted Mathematics: A Kernel-Closed Hamilton Classification and a Mixed-Boundary Rado Study
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.
Proof Engine 2.0: An Evidence-Governed Method for Autonomous Mathematical Research
A complementary project-level method for source inquiry, existing-solution checks, statement correspondence, and the governance of changing mathematical objectives.