A cubic lower bound for the permanent versus the determinant
The permanent–determinant problem asks how large a determinant of affine-linear forms must be to express the m × m permanent. Its size is the determinantal complexity dc(perm); allowing coefficientwise limits of such determinants gives the border determinantal complexity bdc(perm). A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a cubic lower bound for both. This page summarizes the published claim and lists publicly available follow-up work.
Background
- According to the manuscript's introduction, Valiant connected determinant projections to arithmetic formulas and proved the algebraic completeness of the permanent, which makes the growth of dc(perm) a central question of algebraic complexity.
- The same introduction recalls the previous quadratic bounds: Mignon and Ressayre proved dc(perm) ≥ m2/2 in characteristic zero; Cai, Chen and Li extended the quadratic scale to positive characteristic; and Landsberg, Manivel and Ressayre proved the border bound bdc(perm) ≥ m2/2. It places the border question in Mulmuley and Sohoni's geometric complexity theory programme.
The original result
- Claim. There are absolute constants c > 0 and m0 with bdc(perm) ≥ cm3 for every m ≥ m0; one may take c = 1/(5,529,600e) and m0 = 1408 (Theorem 1.1). The same bound holds for exact determinantal complexity, and the manuscript derives cubic lower bounds for the numbers of vertices and edges of affine-linear algebraic branching programs computing the permanent.
- Source. A cubic lower bound for border determinantal complexity of the permanent in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/108.md states that the formalization proves, for m ≥ 1408, that every affine-linear determinant representation of the complex permanent of size n, including coefficientwise limits, satisfies n ≥ m3/(5,529,600e), together with a general supporting theorem for polynomials whose first nonzero homogeneous Taylor term is smooth. The algebraic-branching-program consequences are outside these statements. The Comparator statements are
PermanentCubic.leanandSmoothInitialForm.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates both challenges of this family "full" and records a sandboxed Comparator pass for each. | MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists neither challenge of this family, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-08-26 (v1); v2 later | J. Guo, An n2 log log n Lower Bound for Permanent Circuits with Valid Division (arXiv:2609.29568) | Use (Lean declarations) | Proves lim inf Ldiv(pern)/(n2 log2 log2 n) ≥ 1/12 for permanent circuits with valid division, using Chapter 5 of OpenAI's Ten Advances and classical bounds of Strassen and Baur–Strassen. The abstract states that twelve machine-checked declarations of the Lean development accompanying the September 24 manuscript imply, by a short written argument, the existence of a geometric slice, and that a further written, unformalized application gives Ldiv(pern) ≥ (n2/119790) log2(n/44) for n ≥ 1936. | arXiv preprint (version 2). |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.