Theoretical computer science · Result 108

A cubic permanent–determinant lower bound

1 paperLean

Proves an \(\Omega(n^3)\) lower bound for the border determinantal complexity of the \(n\times n\) permanent over ℂ. Even coefficientwise limits of determinants of affine-linear matrices require matrix size at least \(cn^3\), for an absolute c > 0 and all sufficiently large n; the same bound therefore holds for exact representations.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A cubic lower bound for border determinantal complexity of the permanent

OpenAI · September 24, 2026

We prove that the complex border determinantal complexity of the \(m\times m\) permanent is \(\Omega(m^3)\), allowing arbitrary affine-linear determinant representations and coefficientwise limits. It also gives cubic lower bounds for exact determinantal complexity and for the numbers of vertices and edges in affine-linear algebraic branching programs, including coefficientwise limits with a fixed vertex or edge budget.

Read PDF Download Source

Cite

@misc{OAI:A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026,
  author = {{OpenAI}},
  title = {{A cubic lower bound for border determinantal complexity of the permanent}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026/A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026.pdf}{OAI:A-cubic-lower-bound-for-border-determinantal-complexity-of-the-permanent-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A cubic lower bound for border determinantal complexity of the permanent

Scope

The formalization proves a cubic lower bound for both exact and border determinantal representations of the complex \(m\times m\) permanent. For \(m\ge1408\), every affine-linear determinant representation of size \(n\), including coefficientwise limits, satisfies \(n\ge m^3/(5529600e)\).

A general supporting theorem applies to a polynomial in \(d\ge2\) variables whose first nonzero homogeneous Taylor term has degree \(r\ge2\) and no nonzero singular zero. Its exact and border determinantal sizes are at least \((r-1)(d-1)/(4e)\). The paper's algebraic-branching-program consequences are outside these statements.

Comparator links

Result	Comparator statement
Cubic lower bounds for permanent determinantal complexity	PermanentCubic.lean
Determinantal lower bound from a smooth initial form	SmoothInitialForm.lean

Scope note on GitHub →