How large must a recipe for the permanent be?
How much arithmetic machinery is required to sum every perfect matching?
The permanent looks like the determinant with its minus signs erased. That cosmetic change leads to one of complexity theory’s central mysteries. This manuscript claims the first permanent-specific lower bound above the input count for completely unrestricted division-free arithmetic circuits, plus near-quartic bounds for tree-like formulas—even when valid division is allowed.1manuscript
A concrete starting point
Picture workers being assigned to jobs. In an n-by-n table, the entry in row i and column j is the value of assigning worker i to job j. A legal matching chooses one square from every row and one from every column. Multiply the chosen values, then add the result over every legal matching. That grand total is the permanent.
A 3×3 table has 3! = 6 legal matchings; an n×n table has n!. Yet “many terms” alone does not prove that every computation needs many steps: multiplication can create many terms at once, shared intermediate results can be reused, and subtraction can create then cancel unwanted terms.18manuscript
The paper asks a more precise question: how many arithmetic gates or repeated variable leaves are unavoidable when the answer must be the exact permanent polynomial?
The running permanent is the sum of this product and the other five legal products.
Why older lower-bound ideas hit a wall
The permanent has N = n² input variables, so merely proving that every variable matters gives an Ω(n²) circuit bound. General circuits are directed graphs: one intermediate result may feed many later gates, and intermediate polynomials may have high degree or cancel heavily. Baur–Strassen makes all first derivatives available with only constant-factor circuit overhead, but exploiting those derivatives still requires controlling their shared zero set.2Baur
The obvious gradient-degree argument fails on the full permanent. If two rows are zero, every first derivative vanishes, leaving a large critical component. Newton-polytope volume heuristics also fail because disconnected matching faces factor and develop singular solutions; the actual permanent coefficients are dependent, not generic.4walkthrough
Formulas pose a different problem. They are trees, so they cannot share work, and classical algebraic Nečiporuk arguments already gave cubic-scale bounds. But the final permanent being multilinear does not force unrestricted intermediate formulas to remain multilinear: powers may appear and later cancel. Differentiation also destroys the tree advantage by introducing shared subcomputations.3Kalorkoti8walkthrough
Circuit track: construct a permanent specialization with a small critical cone, then turn gradient degree into a multiplication-gate count. Formula track: show a short matching exposes quadratically many independent coefficient polynomials, then charge that information to repeated leaves.
- 1
Force many critical points into one permanent specialization.
- 2
A depth-q circuit can create only about 2^q independent critical constraints.
- 3
Bézout degree turns that mismatch into a gate lower bound.
- 1
Choose a short matching whose coefficients vary independently.
- 2
A Vandermonde-style Jacobian exposes Ω(n²) degrees of freedom.
- 3
Charge those coefficients through the formula tree and pack matchings.
Track one: critical cones and roots of unity
For a homogeneous degree-d polynomial P, its critical set is where all partial derivatives vanish. If this cone has codimension at least k, a generic k-dimensional input slice and generic k-dimensional output projection produce a square gradient map F: ℂᵏ → ℂᵏ whose only zero is the origin. A generic output then has exactly (d−1)ᵏ preimages.5manuscript
A circuit with q multiplication gates can encode such a fiber using q quadratic gate equations, so Bézout bounds its isolated solutions by 2ᑫ. Reverse-mode differentiation costs at most three multiplications per multiplication in the original circuit. Comparing the two counts yields a lower bound proportional to k log₂(d−1).21manuscript
Build the right polynomial inside one permanent
The basic block is a rectangular matching polynomial: the sum of every d-edge matching between selected row and column sets. Columnwise inclusion–exclusion shows that its critical locus has controlled dimension using the permanent’s actual dependent coefficients—not an imaginary generic replacement. Characteristic zero matters because a leading factorial coefficient must be nonzero.6manuscript
A product of good blocks would be useless: whenever two factors vanish, the product’s whole gradient vanishes. A sum in disjoint variables makes critical codimensions add, but the proof must realize that sum as a specialization of one permanent. Carefully repeated columns weighted by d-th roots of unity cancel every mixed-block matching while preserving each intended within-block matching with nonzero weight.7manuscript
Choosing d ≈ (log₂ n)/4, packing blocks, and slicing the resulting critical cone gives the manuscript’s exact circuit claim: for n ≥ 2¹⁶, C(pern) ≥ (n²/144)(log₂ log₂ n − 3). Thus C(pern) = Ω(n² log log n), which eventually beats the n² input count.19manuscript
Track two: matching coefficients and formula trees
Mark k = 2⌈log₂ n⌉ entries with no repeated row or column and expand the permanent in those marked variables. Each subset of the matching has a coefficient polynomial in the unmarked entries. The key question is not how many coefficients look different, but how many are algebraically independent—how many genuinely separate parameters they carry.23walkthrough
The paper specializes the unmarked matrix so a carefully chosen m²-by-m² Jacobian factors into two Vandermonde evaluation matrices. Its nonzero determinant proves that a matching of only O(log n) marked entries controls at least m² = Ω(n²) independent coefficient polynomials.9manuscript
In a formula tree, mark every node whose subtree contains one of those variables. Long paths with only one marked child compress to a small wrapper; only branching points introduce new outside parameters. A division-free formula with ℓ marked leaves exposes fewer than 4ℓ independent parameters. With valid division, the wrapper becomes a fractional-linear map and the bound becomes fewer than 6ℓ.10manuscript
The n² matrix entries can be packed into Ω(n²/log n) entry-disjoint short matchings. Their leaf charges do not overlap, so they add: division-free formulas require at least n⁴/(128 log₂ n) variable leaves and n⁴/(256 log₂ n) internal gates; valid-division formulas require n⁴/(192 log₂ n) variable leaves and n⁴/(384 log₂ n) gates, for n ≥ 32.25manuscript
Optional technical layer · what the invariants measure
Circuit invariant. Crit(P) = V(∂₁P,…,∂ₘP). If codim Crit(P) ≥ k, generic linear maps W and A give F(u) = A∇P(Wu) with F⁻¹(0) = {0}. Homogeneity makes a generic fiber a complete intersection of k equations of degree d−1, hence degree (d−1)ᵏ. Gate equations and Baur–Strassen give (d−1)ᵏ ≤ 2³ᴸ.22manuscript
Formula invariant. Write f(Y,Z) = Σαcα(Z)Yα. The coefficient transcendence degree tdY(f) is the maximum number of coefficient polynomials with no algebraic relation over ℂ. Lemma 9.1 proves tdY(pern) ≥ (n−2⌈log₂n⌉)² for the chosen matching. Pruning gives tdY(f) ≤ 4ℓ in division-free trees and <6ℓ with valid division.24manuscript26manuscript
Exact scope and formal evidence
The circuit theorem concerns exact symbolic computation over ℂ by fan-in-two +, −, and × circuits. Inputs are not counted as gates; there is no restriction on depth, fan-out, intermediate degree, or cancellation, but division is excluded. The formula theorems count repeated variable leaves in a tree; the division version permits rational intermediate expressions only when every denominator is a nonzero rational function.29manuscript
Permanent.lean is a real formal companion, not an absent certificate. It includes a log-log circuit lower bound and its asymptotic corollary, and separately states the division-free and valid-division formula bounds with their constants. The circuit declaration uses the explicit threshold 2¹⁶; the formula declarations use n ≥ 32.11formal artifact12formal artifact
Stronger-looking lower bounds were already known in restricted models: monotone circuits forbid subtraction and cancellation, while syntactically multilinear formulas require disjoint variable sets at every product gate. Those results do not transfer to the unrestricted models here.14Jerrum15Raz
Most importantly, Ω(n² log log n) is still polynomial. It does not prove that the permanent lacks polynomial-size circuits, and therefore does not prove VP ≠ VNP. The formula result is much larger because a formula is a more restrictive, non-sharing model.16manuscript
Is the claim overhyped?
If correct, these are substantial model-specific lower bounds. They are not the exponential or superpolynomial general-circuit breakthrough that algebraic complexity ultimately seeks.
“Superquadratic unrestricted permanent circuit bound.”
Supported by the released theorem: n² log log n divided by n² grows without bound. “Unrestricted” still means the precisely defined division-free arithmetic-circuit model over ℂ.20manuscript
“Near-quartic formula bound, even with division.”
Supported for valid rational formulas over ℂ, with Ω(n⁴/log n) variable-leaf and gate bounds. It is not a circuit-with-division theorem.27formal artifact
“The first bound of its kind.”
The manuscript’s related-work review supports “first permanent-specific superquadratic bound for unrestricted division-free circuits.” Novelty priority should still be checked by independent experts against the full literature.13manuscript
“The permanent is now proved computationally intractable.”
No. The circuit lower bound remains polynomial and does not rule out polynomial-size circuits or settle VP versus VNP.28manuscript
“Astra established the result.”
This is OpenAI’s attribution. The manuscript, walkthrough, and Lean file are same-release evidence, not independent peer review or reproduction.17announcement
Full bibliography
29 fully annotated sources
- 01 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — pp. 112–116, Theorems 1.1–1.3. The released manuscript and source of the three main bounds; not independent validation. ↩
- 02 · peer-reviewed predecessor
Walter Baur and Volker Strassen. The complexity of partial derivatives — Theoretical Computer Science 22 (1983), pp. 317–330. Supplies constant-overhead simultaneous differentiation used in the circuit track. ↩
- 03 · peer-reviewed predecessor
K. A. Kalorkoti. A Lower Bound for the Formula Size of Rational Functions — SIAM Journal on Computing 14 (1985), pp. 678–687. Classical algebraic Nečiporuk method and cubic determinant formula lower bound, including division. ↩
- 04 · reasoning walkthrough
OpenAI. Reasoning Walkthroughs: Permanent Circuits — Chapter 5, §§5.1–5.6, pp. 20–23. Retrospective route through failed gradient-volume ideas and the final critical-cone construction; not independent evidence. ↩
- 05 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §§4–5, pp. 118–124. Critical-cone slicing, generic-fiber degree, and multiplication-gate bound. ↩
- 06 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §5, Proposition 5.1, pp. 124–127. Columnwise inclusion–exclusion bound for matching-polynomial critical loci. ↩
- 07 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §6, Lemma 6.1, pp. 127–130. Root-of-unity construction cancelling mixed blocks inside one permanent. ↩
- 08 · reasoning walkthrough
OpenAI. Reasoning Walkthroughs: Permanent Formulas — Chapter 6, §§6.1–6.7, pp. 24–27. Retrospective account of the matching-coefficient and valid-division route. ↩
- 09 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §9, Lemma 9.1, pp. 134–138. The two-Vandermonde Jacobian proving quadratic coefficient transcendence degree. ↩
- 10 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §10, pp. 138–142. Matching packing and the formula lower bounds with and without valid division. ↩
- 11 · formal certificate
OpenAI. Permanent.lean — circuit lower bound — lines 20352–20480. Lean declarations for the log-log circuit bound and its asymptotic form. ↩
- 12 · formal certificate
OpenAI. Permanent.lean — formula lower bounds — lines 27684–27738. Lean declarations for division-free and valid-division formula bounds. ↩
- 13 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §12.1 and §12.5, pp. 145–150. Comparison with previous unrestricted and restricted-model bounds. ↩
- 14 · peer-reviewed predecessor
Mark Jerrum and Marc Snir. Some exact complexity results for straight-line computations over semirings — Journal of the ACM 29 (1982), pp. 874–897. Exponential permanent lower bounds in the monotone semiring model, where cancellation is forbidden. ↩
- 15 · peer-reviewed predecessor
Ran Raz. Multi-linear formulas for permanent and determinant are of super-polynomial size — Journal of the ACM 56 (2009). A much stronger bound under syntactic multilinearity, a restriction absent here. ↩
- 16 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §11 and §12.1, pp. 141–147. Determinant comparison, computational-model distinctions, and scope limits. ↩
- 17 · official announcement
OpenAI. Ten advances in mathematics — item 5. Evidence for OpenAI’s attribution and framing only; not independent mathematical review. ↩
- 18 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — Introduction, pp. 113–116. Defines the exact circuit and formula models and explains their relation to the central VP-versus-VNP problem. ↩
- 19 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — Theorem 1.1, p. 113. Exact log-log circuit lower bound and threshold. ↩
- 20 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — Theorem 1.1 and §12.1. Supports the superquadratic circuit characterization within the stated model. ↩
- 21 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §4, pp. 118–124. Gate-equation Bézout bound and reverse-mode differentiation. ↩
- 22 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §4, Lemmas 4.1–4.3. Technical critical-cone and fiber-degree statement. ↩
- 23 · reasoning walkthrough
OpenAI. Reasoning Walkthroughs: Permanent Formulas — Chapter 6, §§6.3–6.4. Discovery account for the logarithmic matching and tensor-product Jacobian. ↩
- 24 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §9, Lemma 9.1. Technical coefficient-transcendence bound. ↩
- 25 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §§10.1–10.3. Exact packing count and both formula bounds. ↩
- 26 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §8 and §10. Coefficient transcendence degree and marked-tree pruning bounds. ↩
- 27 · formal certificate
OpenAI. Permanent.lean — valid-division formula theorem — lines 27699–27738. Formal statement of the valid-division formula constants. ↩
- 28 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — §11 and §12.1. Explains why the bounds do not settle polynomial circuit size or VP versus VNP. ↩
- 29 · primary manuscript
OpenAI. Permanent Circuit and Formula Lower Bounds — Introduction, computational-model definitions. Exact gate, leaf, cancellation, and valid-division conventions. ↩