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-07	realopjt/foulkes-sixth-power-check (GitHub, commit 7280ec4)	Partial verification (base range)	An independent checker written in Rust works with weight multiplicities obtained from Newton's identity and converts them to Schur multiplicities by Weyl alternation at the end, instead of the manuscript's Schur-basis recurrences. It reports that for every b from 6 to 25 and every partition of 6b with at most six parts the target multiplicity is at least the source multiplicity, with no violations and with dimension checks on both sides, and that the manuscript's own verification script, rerun unchanged, reproduces all 62 published output rows. The README states that the certificate layer for 26 ≤ b ≤ 149 and the general argument are not checked, and that both computations use Newton's identity.	Repository result (checked against commit adc7f12 of openai/math); the README states that it was prepared with Claude (Anthropic) and that the mathematics and the original computation are OpenAI's.
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.
2026-10-10	cert-machine, openai/math lane F, check F-369	Partial verification (finite certificate)	Recomputes the inequality for b from 6 to 12 at every partition, by a route independent of the manuscript's programs, and reproduces the corresponding rows of the manuscript's table; it also checks every band coefficient for b from 26 to 29 (467,068 coefficients, none negative). The range b from 13 to 25 was not run for cost, and the certificate step for the partitions outside the band at b from 26 to 29 was not re-implemented, so the recorded verdict for the item is refused; the record states that a separate run reached b = 15.	Repository; the project's ledger records the decided checks (checked 17 October 2026).

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.