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.

Combinatorics · Number theory · Geometry27 mathematical results · 4 methodology papers

Mathematical results 27

A reading route through open problems, classifications and constructive theories.

Erdős #1212Number theory

Infinite paths in the composite-restricted visible lattice

An infinite lattice path answers Erdős’s question; the theorem also prescribes almost every limiting direction in an interval.

Working Paper · ZenodoFull formalization availableFirst public 2026-09-06

Explore this result

Constructive inverse theoryTropical mathematics

A constructive inverse theory for symmetric tropical characteristic polynomials

Which coefficient sequences come from symmetric tropical matrices? A constructive criterion connects realization, reconstruction and parameterized algorithms.

Working Paper · ZenodoFull formalization not yet availableFirst public 2026-09-02

Explore this result

Propp’s Problem 6Combinatorics

Finite-Defect Path Models for Peripheral Benzel Tilings: Propp's Problem 6 and the First Defect Diagonal

An exact tiling formula develops into a finite-defect path model and generating functions for the first defect diagonal.

Working Paper · SSRNFull formalization availableFirst public 2026-08-22

Explore this result

Complete classificationCombinatorics

Hamilton Cycles and Paths in the Noncrossing Partition Refinement Graph

Hamilton cycles and paths in noncrossing partition refinement graphs: a classification for every order, with constructions and parity obstructions.

Working Paper · SSRNFull formalization availableFirst public 2026-07-12

Explore this result

Uniform enumerationCombinatorics

Ballot-Admissible Fibonacci Ribbon Tableaux: Complete Enumeration for Arbitrary Alphabet Size and Fixed-Rank Asymptotics

From a known three-letter case to every alphabet size, with exact counts, fixed-rank asymptotics and a probabilistic limit.

Working Paper · SSRNFull formalization availableFirst public 2026-08-29

Explore this result

A classification-free proofGeometry

A Classification-Free Proof of the Root-Polytope Projection Theorem

A uniform proof of the known root-polytope projection theorem replaces a classification check and gives a rootwise estimate.

Working Paper · ZenodoFull formalization availableFirst public 2026-09-05

Explore this result

Selections introduce different contributions; review levels remain specific to each paper.

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-09-06

2026-09-05

Combinatorics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-09-05

2026-08-04Revised 2026-09-05

Number theory Kernel-OnlyWorking Paper · SSRN

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.

SSRN2026-08-05 Zenodo2026-08-04 Kernel-Only formalization

2026-08-17Revised 2026-08-31

Combinatorics Kernel-OnlyWorking Paper · SSRN

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.

SSRN Zenodo2026-08-17 Kernel-Only formalization

2026-08-22Revised 2026-09-05

Combinatorics Kernel-OnlyWorking Paper · SSRN

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.

SSRN Zenodo2026-08-22 Kernel-Only formalization

2026-09-04

Combinatorics Kernel-OnlyWorking Paper · Zenodo

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.

Zenodo2026-09-04 Kernel-Only formalization

2026-08-29Revised 2026-08-31

Combinatorics Kernel-OnlyWorking Paper · SSRN

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.

SSRN Zenodo2026-08-29 Kernel-Only formalization

2026-08-31

Combinatorics Kernel-OnlyWorking Paper · SSRN

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.

SSRN Zenodo2026-08-31 Kernel-Only formalization

2026-09-05

Geometry Kernel-OnlyWorking Paper · Zenodo

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.

Zenodo2026-09-05 Kernel-Only formalization

2026-09-02Revised 2026-09-03

Tropical mathematics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-09-02

2026-08-25

Combinatorics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-08-25

2026-09-05

Combinatorics Kernel-OnlyWorking Paper

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.

Kernel-Only formalization

2026-08-25

Combinatorics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-08-25

2026-03-11Revised 2026-08-31

Combinatorics Paper CloseWorking Paper · SSRN

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.

SSRN2026-06-04 Zenodo2026-03-11 Code & materials

2026-05-22

Combinatorics Paper CloseWorking Paper · Zenodo

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.

Zenodo2026-05-22 Code & materials

2026-07-12Revised 2026-08-31

Combinatorics Kernel-OnlyWorking Paper · SSRN

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.

SSRN Zenodo2026-07-12 Kernel-Only formalization

2026-09-06Revised 2026-09-07

Number theory Kernel-OnlyWorking Paper · Zenodo

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).

Zenodo2026-09-06 Kernel-Only formalization

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Additive Augmentation Gaps Do Not Force Log-Concavity

Counterexamples to Xie and Xu's rank-dependent log-concavity conjecture for independence systems, including a 13-element example and families with asymptotically full rank and vanishing log-concavity ratios.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Real-Rooted Neighbourhood Polynomials of Unbounded Degree

Trees of every maximum degree whose common-neighbour subset-counting polynomials have only simple negative roots; a solution to Day's question and a full fixed-degree coefficient-limit classification.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Nonnegative Cyclotomic Products and Square-Sided Dice

Cyclotomic polynomials encode primitive roots of unity. A complete classification of nonnegative products in a two-prime-power family resolves a conjecture on relabeling dice whose number of sides is a square. A sharp degree bound for polynomial multipliers and all equality cases are also established.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Peaks and Gaussian Limits for Powered Binomial-Sum Ratios

Ratios of truncated binomial power sums to full sums in shorter rows: the conjectured maximum asymptotic, shifted integer peaks and a Gaussian limiting profile for fixed positive powers and weights, with strict log-concavity for the square power.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Independent-Set Threshold Games and Geodetic Removal on Odd Cycles

Geodetic removal ends when the remaining vertices cannot generate the graph by repeatedly adjoining shortest paths. The second player wins on every odd cycle of order at least five. Changing the cyclic order connects this result to a dynamic pairing strategy for selecting a set containing a prescribed number of pairwise nonadjacent vertices, with exact winning times on paths and cycles.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Four-Part Multiset Resolutions of Cylindrical Graphs

Minimum distances to partition parts are recorded without labels, retaining repeated distances. For prisms formed from two equal cycles joined at corresponding vertices, four parts suffice and are optimal whenever the cycle length is at least ten. Explicit cycle profiles give exact height limits for specified cylindrical partitions. Five-part bounds cover prisms of cycle length eight and nine, and cylinders with at least two layers and even circumference at least twelve.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Uniform Sparse Asymptotics for Crossword Rook Placements

A complete rook placement chooses one cell in every maximal uninterrupted white segment of each row and column. For an n-by-n grid with k uniformly chosen black cells, the mean number of placements is asymptotic to n!(n/36)^k when k grows more slowly than the square root of n. When k/sqrt(n) tends to a finite value lambda, the normalized mean tends to exp(-27 lambda^2/50). The component analysis also gives spatial laws for uniformly chosen grid-placement pairs and existence bounds for uniform grids.

Zenodo2026-09-06

2026-09-06

Combinatorics Paper CloseWorking Paper · Zenodo

Matchings and Independence in Bounded-Occupancy Token Graphs

Configurations place a fixed number of indistinguishable tokens on graph vertices; one move transfers one token along one edge. With unrestricted occupancy or a common even occupancy bound, if a bipartite base graph has disjoint edges covering one part, the configurations with even total occupancy on that part form a maximum independent set: no one-step move joins two of them, and no larger set has that property. This proves the supertoken independence conjecture. The paper also gives sufficient conditions for unequal vertex capacities and explicit odd-capacity counterexamples.

Zenodo2026-09-06

2026-09-07

Combinatorics Paper CloseWorking Paper · Zenodo

Stable Consecutive Patterns and Chain Clusters

A consecutive permutation pattern specifies the relative order of a block of distinct adjacent letters. We classify the patterns whose occurrence distribution is unchanged when the numbers of copies assigned to the letters are permuted. The criterion is that each connected group of overlapping occurrences forces one total order on its positions. We give a sharp finite pair-count test, nonmonotone stable examples such as 12435, exact-position refinements and a joint criterion for same-length patterns beginning with their smallest letter.

Zenodo2026-09-07

2026-09-07

Combinatorics Paper CloseWorking Paper · Zenodo

Recognizing Recursive Designs from Their Incidence Structure

A design here consists of distinct, equally sized point subsets, called blocks, of size at least two; every point lies in the same positive number of blocks. For two recursive constructions, we recover hidden parts from point-block membership alone and determine all block-preserving point permutations, called automorphisms. This proves two conjectures of Amarra, Devillers and Praeger and classifies the exceptions. Integer relations among the membership vectors also recover the input of the single-partition construction without prior parameter information. Fixed finite construction recipes inherit the group and isomorphism results.

Zenodo2026-09-07

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)

Internally reviewed and publicly released. Complete formalization of the principal conclusions is not yet established; errors may 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.

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

Sort

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 · First public: newest first · Records updated 2026-09-07

2026-09-05

Mathematical research methodsWorking Paper · Zenodo

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.

Zenodo2026-09-05

2026-08-05Revised 2026-08-31

Mathematical research methodsWorking Paper · SSRN

Beyond Kernel Verification: The Missing Engineering Layer of Mathematics

A methodological account of statement correspondence, evidence, and the engineering surrounding kernel verification.

SSRN2026-08-06 Zenodo2026-08-05

2026-07-29Revised 2026-08-31

Mathematical research methodsWorking Paper · SSRN

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.

SSRN2026-08-06 Zenodo2026-07-29

2026-06-06Revised 2026-09-06

Mathematical research methodsWorking Paper · SSRN

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.

SSRN2026-06-26 Zenodo2026-06-06

Back to research home