Foulkes' conjecture

Foulkes' conjecture (1950) compares two ways of composing symmetric powers. For a finite-dimensional complex vector space V and integers 1 ≤ a ≤ b, it asks for a GL(V)-equivariant injection Sym^a(Sym^b V) ↪ Sym^b(Sym^a V). Equivalently, the plethysm difference h_b[h_a] − h_a[h_b] is Schur-positive. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 25 September 2026, make claims on this problem. One claims the case a = 6; the other claims surjectivity of the canonical Foulkes–Howe map for b ≥ a(a − 1). This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the introduction of Foulkes' conjecture for the sixth symmetric power:
  • Origin and small cases. The conjecture comes from Foulkes' study of concomitants. For binary forms, Hermite reciprocity gives an isomorphism of the two sides. The case a = 2 follows from Thrall's decomposition formulas, and Dent and Siemons proved a = 3.
  • The canonical map. McKay proved that injectivity of the canonical Foulkes–Howe map for every V at a seed (a, b₀) propagates to all b ≥ b₀. The computation of Müller and Neunhöffer at (4, 4) then gives a = 4, and that of Cheung, Ikenmeyer and Mkrtchyan at (5, 6) gives a = 5.
  • Kernels at the diagonal. The canonical maps at (5, 5) and (6, 6) have nonzero kernels in suitable dimensions, so canonical injectivity is stronger than Foulkes' multiplicity comparison.
  • Computations. Evseev, Paget and Wildon verified the multiplicity inequalities when the two parameters sum to at most 19, including the sixth case through b = 13.
  • Asymptotics. Brion proved eventual truth for fixed a, and gave a dimension-dependent bound for surjectivity of the canonical map in the opposite direction.

The original results

• The sixth case (25 September 2026). Theorem: for every integer b ≥ 6 and every finite-dimensional complex V there is a GL(V)-equivariant injection Sym⁶(Sym^b V) ↪ Sym^b(Sym⁶ V). The manuscript presents this as resolving the case a = 6 positively, with no restriction on dim V.
  • Method, as described: exact character calculations, in the spirit of the character-deflation recurrence of Evseev, Paget and Wildon, combined with bounds on families of multiplicities. Together they leave a small band for exact comparison, which finite certificates settle.
  • Reliance on the companion. The main route uses the companion's quadratic stabilization for b ≥ 30 and the finite comparisons through b = 29. The manuscript also retains an independent route: its certificate programs run through b = 149, and a chart calculation with polarization proves canonical surjectivity for b ≥ 150.
  • Programs. The complete programs are printed in the appendices. The manuscript folder supplies them with reference outputs and a reproduction script. The README describes a read-only check (verify_computations.py --check) and a full run of both C++ programs that compares their output streams with the reference bytes.
• Quadratic stabilization (25 September 2026). The manuscript Quadratic stabilization of the canonical Foulkes–Howe map claims that, for every finite-dimensional complex V, the canonical map Sym^b(Sym^a V) → Sym^a(Sym^b V) is surjective whenever a ≥ 2 and b ≥ a(a − 1). The bound is independent of dim V.
• Sources. Commit 1581d4c of the openai/math repository:
  • Foulkes' conjecture for the sixth symmetric power (with its verification/ directory);
  • Quadratic stabilization of the canonical Foulkes–Howe map.
• Formalization, as described by the repository.
  • The scope note lean/docs/210.md links the stabilization manuscript. The formalized result is surjectivity of the canonical averaged Foulkes–Howe map for every finite-dimensional complex V, a ≥ 2 and b ≥ a(a − 1). It also covers the bijective a = 1 case, the vanishing-on-products consequence, and the reverse equivariant embedding. The note adds: "The sixth-power specialization is covered for b ≥ 30; the companion's full range b ≥ 6 is not included."
  • The Comparator challenge FoulkesHowe.lean states canonical_foulkes_howe_surjective.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 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 the family "partial": quadratic stabilization is stated, while the sixth case of Foulkes' conjecture is reached only for b ≥ 30, and the equivariant embedding is only implicit (the dual of surjectivity). Records a sandboxed Comparator pass for FoulkesHowe.	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 (time-outs, fuel, memory, errors) does not list FoulkesHowe. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the FoulkesHowe solution (301 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.

Notes

• The kernel checks above concern the formal statement canonical_foulkes_howe_surjective. The sixth case for 6 ≤ b ≤ 29 rests on the manuscript's finite computations, which are not part of the formal statement.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.