AI Proof WatchKeep up with AI contributions

Ten Advances in Mathematics and Theoretical Computer Science

OpenAI

A recursive k-edge-coloring of a complete graph without a monochromatic triangle gives Rₖ(3)≥(c k^(1/3)/log k)^k for all sufficiently large k. Thus log Rₖ(3)=Θ(k log k).

Sources for this record

What was already known

Prior product constructions gave fixed-base exponential lower bounds. Erdős #183 asked whether the base could grow with k.

AI involvement AI-led

OpenAI attributes the coloring argument and Lean formalization to Astra; humans selected the problem and prepared the manuscript.

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

Importance Notable

Shows superexponential growth and resolves the stated scale question.

Limitations

The leading constant in the exponent remains open. A chapter-specific human review follows the recursion but is not a complete independent proof check; the Lean result is source-reported.

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 9 discussion

Checker
Chapter 9 human reviewers in the Sienicki et al. review corpus
Scope
recursive coloring, palette count and asymptotic conversion
Basis
Reported by the linked checker
Evidence source

Formal checking

Lean 4.32.0 formal certificate in MulticolorTriangleRamsey.lean; comparator target for ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit; manifest reports zero sorry and only standard axioms. main_results entry ErdosProblems.MulticolourTriangleRamsey.erdos_problem_183_explicit; status and axioms

Checker
OpenAI ten-proofs project, Lean kernel and Comparator configuration
Scope
explicit superexponential lower bound for multicolor triangle Ramsey numbers
Basis
Reported by the linked checker
Evidence source

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

Human understanding Full

The Chapter 9 assessment follows the palette recursion, triangle-free invariant and asymptotic interpolation; the manuscript gives a readable mechanism.

Correction and publication history