Bipartite Exact Matching in P
The Exact Matching problem asks whether a bipartite graph with edges colored red and blue admits a perfect matching with exactly red edges. Introduced by Papadimitriou and Yannakakis in 1982, it has been in randomized polynomial time since Mulmuley-Vazirani-Vazirani (1987) while membership in P stayed open for four decades. The paper claims a deterministic polynomial-time algorithm, replacing probabilistic amplification with deterministic evaluations.
- Result
- Proved
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Algorithms; derandomization
- Posed by
- Christos Papadimitriou, Mihalis Yannakakis
- Year posed
- 1982
- Years open
- 44y
- Solved
- 2026-04-02
- Model
- GPT-5.4 Pro, Claude Opus 4.6, Aristotle
- Vendor
- OpenAI, Anthropic, Harmonic
- Collaborators
- Yuefeng Du
- Verification
- Unreviewed
- Publication
- Preprint
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
GPT-5.4 Pro assisted with theoretical route selection and problem reduction: identifying viable proof strategies, formulating equivalent reformulations of the main conjecture, and narrowing the search space. Claude Opus 4.6 (via Claude Code) ran rapid iterative computational experiments that tested conjectures and produced counterexamples to failed approaches. Lean 4 with Mathlib served as the formal verification backend, with Harmonic's Aristotle discharging proof obligations during the formalization.
Verification
A single-author preprint claiming a forty-year-open result. The paper reports a Lean 4/Mathlib formalization with Aristotle assisting, but no independent expert has reviewed the claim; entered as a candidate pending community scrutiny.