arxiv: 2604.01571 · v3 · submitted 2026-04-02 · 💻 cs.DM · cs.CC· cs.DS

Recognition: no theorem link

Bipartite Exact Matching in P

Yuefeng Du

Authors on Pith no claims yet

Pith reviewed 2026-05-13 21:13 UTC · model grok-4.3

classification 💻 cs.DM cs.CCcs.DS

keywords exact matchingbipartite graphsdeterministic algorithmbrace decompositionvandermonde determinantnonvanishing theoremtight-cut decompositionaffine slice

0 comments

The pith

The Exact Matching problem on bipartite graphs admits a deterministic O(n^6) algorithm

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that Exact Matching—deciding whether a red-blue edge-colored bipartite graph has a perfect matching with exactly t red edges—can be solved deterministically in polynomial time. Only randomized algorithms were previously known for this problem posed in 1982. The central step is the Affine-Slice Nonvanishing Theorem, which proves that a Vandermonde-weighted determinant polynomial is nonzero on the exact-t fiber of any bipartite brace whenever that fiber is nonempty. Structural induction on McCuaig's brace decomposition, together with positivity arguments for exceptional families and closure tools for superfluous edges, reduces the problem to checking this nonvanishing condition on smaller blocks, producing the O(n^6) bound. A Lean 4 formalization confirms the reduction to eight explicit hypotheses.

Core claim

We establish the Affine-Slice Nonvanishing Theorem (ASNC) for all bipartite braces: a Vandermonde-weighted determinant polynomial is nonzero whenever the exact-t fiber is nonempty. This yields a deterministic O(n^6) algorithm for Exact Matching on all bipartite graphs via the tight-cut decomposition into brace blocks. The proof proceeds by structural induction on McCuaig's brace decomposition. We handle the McCuaig exceptional families via a parity-resolved cylindric-network positivity argument, the replacement determinant algebra, and the narrow-extension cases (KA, J3 to D1). For the superfluous-edge step, we introduce two closure tools: a matching-induced Two-extra Hall theorem that the n

What carries the argument

Affine-Slice Nonvanishing Theorem (ASNC): the assertion that a Vandermonde-weighted determinant polynomial remains nonzero on the exact-t fiber of a bipartite brace whenever that fiber is nonempty, used to certify existence of the desired matching via algebraic nonvanishing after brace decomposition

If this is right

Exact Matching on bipartite graphs moves from randomized polynomial time to deterministic O(n^6) time
Any bipartite graph decomposes via tight cuts into braces on which the nonvanishing theorem applies directly
Exceptional families are resolved by parity-resolved positivity on cylindric networks and narrow-extension cases
Superfluous edges are eliminated by the Two-extra Hall theorem for rank-(m-2) branches and the q-circuit lemma for rank-(m-1) branches
The entire argument reduces to eight explicit hypotheses that are machine-checked in Lean 4

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The algebraic closure tools developed here may apply to other constrained matching problems that admit similar rank or fiber analyses
If the same nonvanishing identity holds for non-bipartite braces, the deterministic algorithm could extend beyond bipartite graphs
Faster determinant evaluation or coarser decompositions could lower the O(n^6) exponent without changing the nonvanishing core
The result demonstrates how structural induction on graph decompositions can derandomize algebraic matching algorithms

Load-bearing premise

The structural induction on McCuaig's brace decomposition covers every case without gaps, including all exceptional families and the superfluous-edge rank branches

What would settle it

A bipartite brace containing a nonempty exact-t fiber for which the corresponding Vandermonde-weighted determinant polynomial is identically zero

Figures

Figures reproduced from arXiv: 2604.01571 by Yuefeng Du.

**Figure 1.** Figure 1: Proof dependency structure. The algebraic chain (left) and structural tools (right) both feed into the reduction theorem, yielding the main result. to a parity-resolved cylindric-network positivity argument via width-2 path and cyclic branch factorization. 1.5. Organization. Section 2 establishes notation and the Vandermonde specialization. Section 3 presents the structural induction framework based on bra… view at source ↗

read the original abstract

The Exact Matching problem asks whether a bipartite graph with edges colored red and blue admits a perfect matching with exactly $t$ red edges. Introduced by Papadimitriou and Yannakakis in 1982, the problem has resisted deterministic polynomial-time algorithms for over four decades, despite admitting a randomized solution via the Schwartz-Zippel lemma since 1987. We establish the Affine-Slice Nonvanishing Theorem (ASNC) for all bipartite braces: a Vandermonde-weighted determinant polynomial is nonzero whenever the exact-$t$ fiber is nonempty. This yields a deterministic $O(n^6)$ algorithm for Exact Matching on all bipartite graphs via the tight-cut decomposition into brace blocks. The proof proceeds by structural induction on McCuaig's brace decomposition. We handle the McCuaig exceptional families via a parity-resolved cylindric-network positivity argument, the replacement determinant algebra, and the narrow-extension cases (KA, $J3 \to D1$). For the superfluous-edge step, we introduce two closure tools: a matching-induced Two-extra Hall theorem that resolves the rank-$(m-2)$ branch via projective-collapse contradiction, and a distinguished-state $q$-circuit lemma that eliminates the rank-$(m-1)$ branch entirely by showing that any minimal dependent set containing the superfluous state forces rank $m-2$. A Lean 4 formalization accompanies the paper. The formalization reduces the main theorem to eight explicit hypotheses corresponding to results proved here and in McCuaig (2001), with all algebraic tools, the induction skeleton, and the combinatorial infrastructure fully machine-checked.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Du claims a deterministic O(n^6) algorithm for bipartite exact matching via a new Affine-Slice Nonvanishing Theorem and Lean-checked induction on McCuaig braces, but the proof reduces to eight unverified hypotheses.

read the letter

The headline result is a deterministic polynomial-time algorithm for the exact matching problem on bipartite graphs, which has been open since 1982. If the argument holds, it replaces the 1987 randomized Schwartz-Zippel approach with an explicit O(n^6) procedure that works for every bipartite graph via tight-cut decomposition into braces. That is the one thing a colleague needs to know first. The paper introduces the Affine-Slice Nonvanishing Theorem together with two closure tools (the matching-induced Two-extra Hall theorem and the distinguished-state q-circuit lemma) that are not in the earlier literature. The Lean 4 formalization machine-checks the induction skeleton, the algebraic machinery, and the combinatorial infrastructure, which is real, reproducible work and keeps internal circularity low. It also correctly cites McCuaig 2001 as the external structural fact rather than re-proving it. Those are the concrete strengths. The soft spots sit exactly where the stress-test note flags them. The main theorem is reduced to eight explicit hypotheses, and the paper's own arguments for the exceptional families (parity-resolved cylindric-network positivity, replacement determinant algebra, narrow-extension cases) and the superfluous-edge rank branches are not fully machine-checked. Any gap in one of those case-specific positivity or closure arguments would leave the nonvanishing claim open for some braces, so the deterministic reduction would not cover all bipartite graphs. The formalization is helpful but does not close the loop. This paper is for researchers in algorithmic graph theory and derandomization who care about exact-constraint matching. A reader who wants to see the new algebraic and combinatorial tools will find usable material even before the hypotheses are settled. It deserves a serious referee because the problem is central, the formalization is present, and the claimed result is sharp enough to justify referee time. I would send it out for review rather than desk-reject it.

Referee Report

1 major / 0 minor

Summary. The manuscript claims to resolve the Exact Matching problem on bipartite graphs in deterministic polynomial time. It establishes the Affine-Slice Nonvanishing Theorem (ASNC) asserting that a Vandermonde-weighted determinant polynomial is nonzero whenever the exact-t fiber is nonempty, for all bipartite braces. The proof uses structural induction on McCuaig's brace decomposition, handling exceptional families via parity-resolved cylindric-network positivity, replacement determinant algebra, and narrow-extension cases (KA, J3→D1), together with two closure tools for superfluous edges (matching-induced Two-extra Hall theorem resolving rank-(m-2) via projective-collapse contradiction, and distinguished-state q-circuit lemma eliminating rank-(m-1)). A Lean 4 formalization machine-checks the induction skeleton, algebraic tools, and combinatorial infrastructure while reducing the main theorem to eight explicit hypotheses.

Significance. If the result holds, it provides the first deterministic polynomial-time algorithm for Exact Matching, a problem open since 1982, via an O(n^6) procedure based on tight-cut decomposition into brace blocks. This would be a major advance in algorithmic graph theory and algebraic combinatorics. The machine-checked formalization of the induction skeleton and algebraic machinery is a clear strength that increases confidence in the infrastructure.

major comments (1)

[Formalization and induction skeleton] The structural induction establishing ASNC for all braces reduces, per the Lean formalization, to eight explicit hypotheses that include the case-specific positivity arguments for McCuaig exceptional families (KA, J3→D1) and the two closure tools for superfluous-edge rank branches. The manuscript should provide an explicit enumeration mapping each of these eight hypotheses to the corresponding lemma or theorem proved in the text (or cited from McCuaig 2001) so that completeness of coverage for all exceptional families and rank-(m-2), rank-(m-1) branches can be directly verified.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback on our manuscript. We address the single major comment below.

read point-by-point responses

Referee: [Formalization and induction skeleton] The structural induction establishing ASNC for all braces reduces, per the Lean formalization, to eight explicit hypotheses that include the case-specific positivity arguments for McCuaig exceptional families (KA, J3→D1) and the two closure tools for superfluous-edge rank branches. The manuscript should provide an explicit enumeration mapping each of these eight hypotheses to the corresponding lemma or theorem proved in the text (or cited from McCuaig 2001) so that completeness of coverage for all exceptional families and rank-(m-2), rank-(m-1) branches can be directly verified.

Authors: We agree that an explicit mapping will improve readability and allow direct verification of coverage. In the revised version we will insert a new subsection (in the formalization section) containing a table that lists each of the eight hypotheses, states its precise statement, and gives the corresponding lemma/theorem number or McCuaig citation that discharges it. This table will explicitly address the KA and J3→D1 positivity arguments as well as the two closure tools for the rank-(m-2) and rank-(m-1) branches. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained against external benchmarks

full rationale

The Affine-Slice Nonvanishing Theorem is established by structural induction on McCuaig's 2001 brace decomposition (an external theorem) together with new parity-resolved positivity arguments, replacement determinant algebra, narrow-extension cases, the Two-extra Hall theorem, and the q-circuit lemma. The Lean formalization explicitly reduces the main result to eight hypotheses that are either proved in the present paper or cited from McCuaig (2001); none of these steps reduce by construction to a self-definition, a fitted parameter renamed as a prediction, or a load-bearing self-citation chain. The central claim therefore retains independent algebraic and combinatorial content.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on McCuaig's brace decomposition as an external combinatorial fact, standard properties of Vandermonde determinants and linear algebra over fields, and the correctness of the newly introduced closure lemmas; no free parameters or invented entities are introduced.

axioms (2)

domain assumption McCuaig's brace decomposition theorem for bipartite graphs
The induction is performed on the structural decomposition established in McCuaig 2001.
standard math Nonvanishing criteria for Vandermonde-weighted determinant polynomials
Invoked to establish the Affine-Slice Nonvanishing Theorem.

pith-pipeline@v0.9.0 · 5582 in / 1450 out tokens · 58105 ms · 2026-05-13T21:13:38.001469+00:00 · methodology

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

A hierarchy of edge-weight symmetries in perfect matchings
math.CO 2026-04 unverdicted novelty 7.0

A matching-covered non-bipartite graph exists where every edge lies in some minimum-weight and some maximum-weight perfect matching, yet not all perfect matchings have identical weight.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages · cited by 1 Pith paper · 1 internal anchor

[1]

Anthropic,Claude Opus 4.6 model card, Technical report, 2026

work page 2026
[2]

Aristotle: IMO-level Automated Theorem Proving

T. Achim et al.,Aristotle: IMO-level automated theorem proving, arXiv:2510.01346, 2025

work page internal anchor Pith review arXiv 2025
[3]

Appel and W

K. Appel and W. Haken,Every planar map is four colorable, I: Discharging, Illinois Journal of Mathematics, 21(3):429–490, 1977

work page 1977
[4]

E. H. Bareiss,Sylvester’s identity and multistep integer-preserving Gaussian elimina- tion, Mathematics of Computation, 22(103):565–578, 1968

work page 1968
[5]

Birkhoff,Three observations on linear algebra, Univ

G. Birkhoff,Three observations on linear algebra, Univ. Nac. Tucum´ an Rev. Ser. A, 5:147–151, 1946

work page 1946
[6]

M. H. de Carvalho, C. L. Lucchesi, and U. S. R. Murty,On a conjecture of Lov´ asz concerning bricks, I: The characteristic of a matching covered graph, Journal of Com- binatorial Theory, Series B, 85(1):94–136, 2002

work page 2002
[7]

Edmonds,Maximum matching and a polyhedron with0,1-vertices, Journal of Re- search of the National Bureau of Standards B, 69:125–130, 1965

J. Edmonds,Maximum matching and a polyhedron with0,1-vertices, Journal of Re- search of the National Bureau of Standards B, 69:125–130, 1965

work page 1965
[8]

El Maalouly, R

N. El Maalouly, R. Steiner, and L. Wulf,Exact matching: correct parity and FPT parameterized by independence number, In Proc. ISAAC 2023, LIPIcs 283, pages 28:1–28:15, 2023. 49

work page 2023
[9]

El Maalouly, S

N. El Maalouly, S. Haslebacher, and L. Wulf,On the exact matching problem in dense graphs, In Proc. STACS 2024, LIPIcs 289, pages 33:1–33:17, 2024

work page 2024
[10]

El Maalouly and K

N. El Maalouly and K. Lakis,Exact matching and top-kperfect matching parameter- ized by neighborhood diversity or bandwidth, arXiv:2510.12552, 2025

work page arXiv 2025
[11]

S. A. Fenner, R. Gurjar, and T. Thierauf,Bipartite perfect matching is in quasi-NC, In Proc. 48th Annual ACM STOC, pages 754–763, 2016

work page 2016
[12]

W. T. Gowers, B. Green, F. Manners, and T. Tao,On a conjecture of Marton, Annals of Mathematics, 201(2):515–564, 2025

work page 2025
[13]

Gurjar and T

R. Gurjar and T. Thierauf,A deterministic parallel algorithm for bipartite perfect matching, Communications of the ACM, 63(2):74–81, 2020

work page 2020
[14]

Hall,On representatives of subsets, Journal of the London Mathematical Society, 10(1):26–30, 1935

P. Hall,On representatives of subsets, Journal of the London Mathematical Society, 10(1):26–30, 1935

work page 1935
[15]

R. M. Karp, U. V. Vazirani, and V. V. Vazirani,An optimal algorithm for on-line bipartite matching, In Proc. 22nd Annual ACM STOC, pages 352–358, 1990

work page 1990
[16]

A. V. Karzanov,Maximum matching of given weight in complete and complete bipar- tite graphs, Cybernetics, 23(1):8–13, 1987

work page 1987
[17]

Kothari and S

P. Kothari and S. Narain,Tight cuts in matching covered graphs, Journal of Combi- natorial Theory, Series B, 2024

work page 2024
[18]

Lam and P

T. Lam and P. Pylyavskyy,Total positivity in loop groups, I: whirls and curls, Ad- vances in Mathematics, 230(3):1222–1271, 2012

work page 2012
[19]

Lov´ asz,On determinants, matchings, and random algorithms, In FCT ’79, pages 565–574, Akademie-Verlag, 1979

L. Lov´ asz,On determinants, matchings, and random algorithms, In FCT ’79, pages 565–574, Akademie-Verlag, 1979

work page 1979
[20]

Lov´ asz and M

L. Lov´ asz and M. D. Plummer,Matching Theory, North-Holland Mathematics Studies 121, Elsevier, 1986

work page 1986
[21]

McCuaig,Brace generation, Journal of Graph Theory, 38(3):124–169, 2001

W. McCuaig,Brace generation, Journal of Graph Theory, 38(3):124–169, 2001

work page 2001
[22]

McCuaig,P´ olya’s permanent problem, The Electronic Journal of Combinatorics, 11(1):R79, 2004

W. McCuaig,P´ olya’s permanent problem, The Electronic Journal of Combinatorics, 11(1):R79, 2004

work page 2004
[23]

Mulmuley, U

K. Mulmuley, U. V. Vazirani, and V. V. Vazirani,Matching is as easy as matrix inversion, Combinatorica, 7(1):105–113, 1987

work page 1987
[24]

OpenAI,GPT-5.4 Pro system card, Technical report, 2026

work page 2026
[25]

C. H. Papadimitriou and M. Yannakakis,The complexity of restricted spanning tree problems, Journal of the ACM, 29(2):285–309, 1982

work page 1982
[26]

Robertson and P

N. Robertson and P. D. Seymour,Graph minors. XX. Wagner’s conjecture, Journal of Combinatorial Theory, Series B, 92(2):325–357, 2004

work page 2004
[27]

J. T. Schwartz,Fast probabilistic algorithms for verification of polynomial identities, Journal of the ACM, 27(4):701–717, 1980

work page 1980
[28]

Svensson and J

O. Svensson and J. Tarnawski,The matching problem in general graphs is in quasi- NC, In Proc. 58th Annual IEEE FOCS, pages 696–707, 2017

work page 2017
[29]

W. T. Tutte,The factorization of linear graphs, Journal of the London Mathematical Society, 22(2):107–111, 1947

work page 1947
[30]

Yuster,Almost exact matchings, Algorithmica, 63(1):39–50, 2012

R. Yuster,Almost exact matchings, Algorithmica, 63(1):39–50, 2012

work page 2012
[31]

Zippel,Probabilistic algorithms for sparse polynomials, In Proc

R. Zippel,Probabilistic algorithms for sparse polynomials, In Proc. EUROSAM ’79, LNCS 72, pages 216–226, 1979. AppendixA.Machine-checked formalization A partial Lean 4 formalization accompanies this paper, with automated proof assistance from Aristotle [2]. The source is available at https://anonymous.4open.science/r/exact-matching-lean-FFD2 What is verif...

work page 1979