AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A Cyclic Polytabloid Proof of Saxl's Conjecture

Can the mathematical statement in A Cyclic Polytabloid Proof of Saxl's Conjecture be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 205)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Cyclic Polytabloid Proof of Saxl's Conjecture'. For every staircase partition, we prove that the tensor square of the corresponding irreducible complex representation of the symmetric group contains every irreducible representation of that group. This proves Saxl's conjecture.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 205). The Lean development was not rebuilt locally.