What was already known
Arnosti proved equality in distribution at capacity one and dominance at capacity two, and conjectured the comparison for larger common capacities.
AI involvement
The project credits OpenAI Codex with the central proof, Lean formalization and verification tooling; a human directed the project, requested simplification and reviewed presentation.
The project credits Codex with the central stochastic-dominance proof, Lean formalization and verification tools. A human directed the project, requested simplification and reviewed presentation. The division of mathematical work supports AI-led involvement.
Importance
Settles the equal-capacity comparison for all finite instances of Arnosti’s random-neighbourhood model.
Limitations
The comparison is over random graphs and algorithm choices; it is not run-by-run dominance, a fixed-graph theorem or a result for unequal capacities. External expert review remains open.
Technical verification
The pinned repository reports a public Lean build of 91 positive modules, including the final source-model theorem, and prints only standard axioms. This is a source-reported machine check of the scoped stochastic-dominance statement; AIProofWatch did not rerun it.
Formal checking
The repository reports a public Lean build of 91 positive modules from commit c521b8d45bfa8a38b60a8e55b5ab104634d48b49, including the final source-model theorem, with only standard axioms printed.
- Checker
- Lean kernel, as reported by MathIsEvenEasier
- Scope
- In Arnosti’s random bipartite matching model with independent uniform job neighbourhoods of prescribed sizes and a common positive integer bin capacity, RANDOM-VERTEX stochastically dominates RANKING in the number of accepted jobs.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. The sources describe human direction and presentation review but do not document a named person explaining the central proof. Few is the default from this evidence gap, not a finding that people cannot understand it.
Correction and publication history
Primary theorem, prior baseline, AI attribution and documented proof scope reviewed for non-notifying local inclusion.
Read this published revision