AI Proof WatchKeep up with AI contributions

Ten Advances in Mathematics and Theoretical Computer Science

OpenAI

For the n×n permanent over the complex numbers and n≥32, Chapter 5 gives at least n⁴/(128 log₂ n) variable leaves for division-free arithmetic formulas and n⁴/(192 log₂ n) for valid rational formulas. A separate circuit lower bound has different scope.

Sources for this record

What was already known

Earlier differentiation and coefficient-counting methods did not give these permanent-specific formula bounds. A formula is a tree, so these are not general circuit bounds.

AI involvement AI-led

OpenAI attributes the argument and Lean formalization to Astra. Humans selected the problem and prepared the manuscript with the model.

OpenAI’s original disclosure assigns the argument and subsequent Lean formalization to Astra; human manuscript preparation is separately credited.

Importance Notable

Improves permanent-specific arithmetic formula lower bounds.

Limitations

The reported main Lean target certifies the rational-formula bound; division-free formula and circuit claims have separate declarations. Human reviews discuss proof structure and parameters without a complete independent reconstruction.

Technical verification Formal (Lean 4.32.0 with Mathlib and Comparator + human)

The project reports a complete Lean certificate for the stated formal theorem. Human assessments have narrower scope; semantic matching and any manuscript gaps remain separately noted.

Independent checking

chapter-specific mathematical review of the published argument, with the limited coverage summarized in the audit. Table 1; Chapter 5 discussion

Checker
Chapter 5 human reviewers in the Sienicki et al. review corpus
Scope
permanent lower-bound proof structure and parameters
Basis
Reported by the linked checker
Evidence source

Formal checking

Lean 4.32.0 formal certificate in Permanent.lean; comparator target for PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound; manifest reports zero sorry and only standard axioms. main_results entry PermanentFormulaLowerBound.permanent_rational_formula_logarithmic_lower_bound; status and axioms

Checker
OpenAI ten-proofs project, Lean kernel and Comparator configuration
Scope
valid rational formula lower bound n^4/(192 log_2 n) for n≥32
Basis
Reported by the linked checker
Evidence source

Checking a formal statement does not establish that it matches the original problem.

Human understanding Full

Three human assessments examine the permanent-specific construction, lower-bound parameter choices and formula/circuit distinctions; they request clearer novelty credit rather than identifying a mechanism gap.

Correction and publication history