Foulkes' conjecture - Revision history

Aftermath bot: Row for an independent Rust check of the base range of the sixth case

2026-10-17T13:58:02Z

Row for an independent Rust check of the base range of the sixth case

← Older revision		Revision as of 06:58, 17 October 2026
Line 25:		Line 25:
	{\| class="wikitable"		{\| class="wikitable"
	! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)		! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
			\|-
			\| 2026-10-07 \|\| [https://github.com/realopjt/foulkes-sixth-power-check/tree/7280ec470b684f5acc00f1581a5afc3456da24a3 realopjt/foulkes-sixth-power-check] (GitHub, commit <code>7280ec4</code>) \|\| 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 6''b'' 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 <code>adc7f12</code> 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 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>FoulkesHowe</code>. \|\| MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.		\| 2026-10-08 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>FoulkesHowe</code>. \|\| MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.

Aftermath bot: Add the cert-machine finite-certificate row with the decided and refused parts

2026-10-17T10:55:46Z

Add the cert-machine finite-certificate row with the decided and refused parts

← Older revision		Revision as of 03:55, 17 October 2026
Line 31:		Line 31:
	\|-		\|-
	\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/FoulkesHowe.json cert-machine], openai/math lane K, run 38019899278 \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>FoulkesHowe</code> solution (301 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. \|\| Repository.		\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/FoulkesHowe.json cert-machine], openai/math lane K, run 38019899278 \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>FoulkesHowe</code> solution (301 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. \|\| Repository.
			\|-
			\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/ee027e39e5b91ba93d24cb895e9302e858a73637/instruments/openaimath/finite/f369_foulkes_six.py 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 [https://github.com/carlostoledo1891/cert-machine/blob/ee027e39e5b91ba93d24cb895e9302e858a73637/certs/openai-math-finite.json ledger] records the decided checks (checked 17 October 2026).
	\|}		\|}

Aftermath bot: New page: Foulkes' conjecture (openai/math family 210), public sources only

2026-10-16T16:45:26Z

New page: Foulkes' conjecture (openai/math family 210), public sources only

New page

'''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 ([https://github.com/openai/math 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''0) propagates to all ''b'' ≥ ''b''0. 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 Sym6(Sym''b'' ''V'') ↪ Sym''b''(Sym6 ''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 (<code>verify_computations.py --check</code>) 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 <code>1581d4c</code> of the openai/math repository:
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Foulkes-Conjecture-for-the-Sixth-Symmetric-Power-September-25-2026 ''Foulkes' conjecture for the sixth symmetric power''] (with its <code>verification/</code> directory);
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Quadratic-Stabilization-of-the-Canonical-Foulkes-Howe-Map-September-25-2026 ''Quadratic stabilization of the canonical Foulkes–Howe map''].
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/210.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/FoulkesHowe.lean FoulkesHowe.lean] states <code>canonical_foulkes_howe_surjective</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>FoulkesHowe</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>FoulkesHowe</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/FoulkesHowe.json cert-machine], openai/math lane K, run 38019899278 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>FoulkesHowe</code> 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 <code>canonical_foulkes_howe_surjective</code>. 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.

[[Category:OpenAI results]]