A neutral schematic of the objects and relations in the statement.
Problem. Does there exist a binary self-dual doubly-even code with parameters \([72,36,16]\)?
1Definitions
Definition 1. Self-dual means C equals its orthogonal complement under the standard binary inner product.
Definition 2. Doubly even means every codeword has weight divisible by four. Minimum distance 16 makes a length-72 Type II code extremal.
2What counts as a solution
Provide a 36 by 72 generator matrix, verify self-duality and doubly-even weights, and certify minimum distance 16; or prove that no such code exists.
1Status
Current status (Existence remains open). The audit found no accepted construction or nonexistence proof for an extremal Type II code of length 72.[4][5][6]
1Records
5 records
Record
Kind
Assessment
Result
Supported
claim · Proposition 1
The audit found no accepted construction or nonexistence proof for an extremal Type II code of length 72.[4][5][6]
Relevance to this problem
For An extremal Type II binary code of length 72, record etc72-claim-open-status (“Existence remains open”) records a bound, answer, status fact, or structural consequence. The record states: The audit found no accepted construction or nonexistence proof for an extremal Type II code of length 72.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
open
Scope
existence of a binary doubly-even self-dual code with parameters [72,36,16]
Sloane posed this exact question in 1973. A Type II code of length 72 has dimension 36, and the Mallows-Sloane bound gives minimum distance at most 16. The requested code would attain that bound.
A 2025 primary preprint on small automorphism groups says that the best known minimum distance for binary self-dual length-72 codes is 12 and that the minimum-distance-16 question remains unsolved. Recent construction work continues to produce Type I and Type II \([72,36,12]\) codes. The primary-source audit through 2026-07-25 found no refereed construction of a \([72,36,16]\) code and no unrestricted exclusion.
The answer is recorded as open. The forced enumerator and automorphism results below are necessary conditions on a witness. Neither condition resolves the unrestricted case.
Result
Reproduced
claim · Computation 1
Gleason's theorem forces 249,849 words of weight 16 and fixes every other weight count.[5]
Relevance to this problem
For An extremal Type II binary code of length 72, record etc72-claim-forced-weight-enumerator (“Every witness has the same weight enumerator”) records a bound, answer, status fact, or structural consequence. The record states: Gleason's theorem forces 249,849 words of weight 16 and fixes every other weight count.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
established
Scope
every binary doubly-even self-dual [72,36,16] code, if one exists
Set
\[
A=x^8+14x^4y^4+y^8,
\qquad
B=x^4y^4(x^4-y^4)^4.
\]
Gleason's theorem and the absence of weights 4, 8, and 12 force
\[
W=A^9-126A^6B+3015A^3B^2-4398B^3.
\]
Expanding gives
\[
\begin{aligned}
W(1,y)={}&1+249849y^{16}+18106704y^{20}+462962955y^{24}\\
&+4397342400y^{28}+16602715899y^{32}+25756721120y^{36}\\
&+16602715899y^{40}+4397342400y^{44}+462962955y^{48}\\
&+18106704y^{52}+249849y^{56}+y^{72}.
\end{aligned}
\]
The coefficients sum to \(2^{36}\), have the required complement symmetry, and are nonnegative. Sloane already listed these values in the 1973 problem statement.
The Assmus-Mattson theorem makes the supports at each nontrivial weight a 5-design. In particular, the 249,849 minimum-word supports form a
\[
5\text{-}(72,16,78)
\]
design because
\[
249849\binom{16}{5}/\binom{72}{5}=78.
\]
These arithmetic conditions are consistent and leave existence open.
For An extremal Type II binary code of length 72, record etc72-claim-automorphism-restrictions (“Only five automorphism groups remain possible”) records a bound, answer, status fact, or structural consequence. The record states: A witness has automorphism group C1, C2, C3, C2 by C2, or C5.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
established
Scope
the full permutation automorphism group of every binary self-dual [72,36,16] code, if one exists
The published exclusions reduce the full permutation automorphism group to
\[
C_1,\quad C_2,\quad C_3,\quad C_2\times C_2,\quad\text{or}\quad C_5.
\]
Borello's 2014 theorem first reduces the list to cyclic groups of orders 1 through 5 and the elementary abelian group of order 4. Yorgov and Yorgov then exclude an element of order 4 by an exhaustive parameterized search, removing \(C_4\).
The restrictions also determine the possible cycle structures. Every involution is fixed-point-free, so it acts as 36 transpositions. Every element of order 3 is fixed-point-free, so it acts as 24 three-cycles. An element of order 5 acts as fourteen 5-cycles and fixes two coordinates.
Earlier primary computations exclude \(C_7\), \(C_3\times C_3\), \(D_{10}\), elements of order 6, \(S_3\), \(A_4\), \(D_8\), and an elementary abelian group of order 8. These results make symmetry-based searches finite in several branches. The trivial-group branch receives no comparable reduction.
Structured searches reach distance 12 or exclude selected symmetry classes; the unrestricted distance-16 question survives.[3][6][10][9]
Relevance to this problem
For An extremal Type II binary code of length 72, record etc72-attempt-construction-and-search-audit (“Construction and search audit”) documents a concrete method, search boundary, or failed route. The record states: Structured searches reach distance 12 or exclude selected symmetry classes; the unrestricted distance-16 question survives.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
completed
Scope
published construction and symmetry-restricted search results bearing on binary self-dual codes of length 72 through 2026-07-25
The audit separated constructions from symmetry exclusions. Yu, Zhu, and Wu use group rings and skew group rings to construct many binary self-dual codes of length 72. Their 2025 paper reports both singly-even and doubly-even codes with minimum distance 12. These are concrete near cases and supply no distance-16 generator matrix.
For the distance-16 target, several searches are exhaustive inside a stated automorphism class. Borello excludes automorphisms of order 6. Feulner and Nebe exclude groups containing \(C_7\), \(C_3\times C_3\), or \(D_{10}\). Yorgov and Yorgov parameterize every possible order-4 case, reduce it by equivalence, and test the remaining branches. Their negative result excludes \(C_4\). The authors' supplement preserves the programs and run organization for that search.
Each exclusion depends on the assumed symmetry. A code with trivial automorphism group remains among the five possible cases, so the union of these searches does not cover every binary Type II code of length 72.
Standard-library Python expands the forced polynomial and checks all coefficients, symmetry, size, distance, and design divisibilities.[5]
Relevance to this problem
For An extremal Type II binary code of length 72, record etc72-artifact-enumerator-replay (“Exact Gleason and 5-design parameter replay”) supplies evidence or a replay used to check the packet. The record states: Standard-library Python expands the forced polynomial and checks all coefficients, symmetry, size, distance, and design divisibilities.
Evidence
ReproducedA computation someone reran from the artifact on this page.
Record state
available
Scope
the unique degree-72 Type II Gleason polynomial whose coefficients at weights 4, 8, and 12 vanish
Join source_lines with LF characters and execute the resulting Python program
Runtime
CPython 3, standard library only
Details
The program represents a homogeneous polynomial by its exponent of \(y\), since every monomial has total degree 72. It expands the four Gleason-basis terms using exact integers and compares the result with the complete expected distribution.
The checks certify 13 nonzero coefficients, coefficient sum \(2^{36}\), complement symmetry \(A_w=A_{72-w}\), and minimum nonzero weight 16. For each nontrivial weight it also evaluates
\[
\lambda_w=A_w\binom{w}{5}/\binom{72}{5}
\]
and verifies integrality. The canonical report has SHA-256 digest `5c244287d06ceec7acd8ef04a7827f61d4214b160a4e7668a3f01db3352c21ea`.
Notes and companion materialContext, examples, and computations
The forced weight enumerator gives strong consistency checks for any construction and useful pruning counts for search certificates.
Original intake status. A 2012 primary paper describes existence as a long-standing open problem and excludes automorphisms of order 6. Current status remains unverified.
Search systematic generator matrices [I|A] with AA^T=I, quotienting coordinate permutations before minimum-distance testing. Preserve the exact automorphism restriction for every negative run.
Trap: exclusions for automorphisms of a given order do not combine into unrestricted nonexistence unless all possible automorphism groups, including the trivial group, are covered.
Recorded example 1. Any witness must contain exactly 249849 codewords of weight 16.
Computational notes
An independent Gleason-basis calculation obtained W=A^9-126A^6B+3015A^3B^2-4398B^3. Its nonzero coefficients begin A_16=249849, A_20=18106704, A_24=462962955 and are all nonnegative; the enumerator test therefore leaves existence open.
How the 5 records connectTyped relations and evidence flowHow the records connect to the problem
ProblemAn extremal Type II binary code of length 72
TheoremDB contributors, “An extremal Type II binary code of length 72,” TheoremDB research memory, snapshot of July 25, 2026. https://theoremdb.org/statements/extremal-type-ii-code-72
This problem includes 5 records joined by 4 typed links, sourced from doi.org[5], current as of July 25, 2026.
1Lean verification
Lean formalization needed
An informal proof is recorded. A Lean formalization still needs to be attached. TheoremDB Researcher can start from the exact statement and pinned world.
The prefilled request prepares the target and checks drafts. It submits the accepted proof and polls verification through any packet-review handoff.
1References
Martino Borello, “The Automorphism Group of an Extremal [72,36,16] Code does not contain elements of order 6”. DOI 10.1109/TIT.2012.2211095. arXiv:1203.3321 (2012). Generated after checking Borello, The Automorphism Group of an Extremal [72,36,16] Code Does Not Contain Elements of Order 6, 2012. ↗preprint · primary source · arXiv:1203.3321v2 · checked 2026-08-01Source use: original summary.For An extremal Type II binary code of length 72: CC0 candidate record based on a primary paper and an independent Gleason-polynomial calculation.
Martino Borello, The automorphism group of a self-dual [72,36,16] code is not an elementary abelian group of order 8, Finite Fields and Their Applications 25 (2014), 1-7. Martino Borello, Finite Fields and Their Applications 25 (2014), 1-7, Theorem 1.1 and final exclusion; combined with Vassil Yorgov and Daniel Yorgov, IEEE Transactions on Information Theory 60(6) (2014), 3302-3307, DOI 10.1109/TIT.2014.2313697. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes an elementary abelian automorphism group of order eight.Also cited at Martino Borello, Finite Fields and Their Applications 25 (2014), 1-7.
Vassil Yorgov and Daniel Yorgov, The automorphism group of a self-dual [72,36,16] code does not contain Z4, IEEE Transactions on Information Theory 60(6) (2014), 3302-3307. Yorgov and Yorgov 2014, parameterization and exhaustive order-4 search; supplementary run materials at https://users.pfw.edu/yorgovd/code3/index.html; construction comparison from DOI 10.1007/s40314-024-03056-z. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes cyclic automorphisms of order four from a length-72 extremal code.Also cited at Vassil Yorgov and Daniel Yorgov, IEEE Transactions on Information Theory 60(6) (2014), 3302-3307.
Carolin Hannusch and Sándor Roland Major, On Small Automorphism Groups of Binary Self-Dual Codes, Preprints.org 202506.2100, version 1 (2025). Version 1, Section 6; the page labels the manuscript unreviewed. ↗preprint · primary source · version 1, posted 2025-06-25 · checked 2026-07-25Source use: citation only.Reports, in an unreviewed manuscript, a reduction to five possible automorphism groups for any length-72 extremal code.Also cited at On Small Automorphism Groups of Binary Self-Dual Codes, 2025, Section 6.
Packet source. N. J. A. Sloane, Is there a (72,36) d=16 self-dual code?, IEEE Transactions on Information Theory 19(2) (1973), 251. N. J. A. Sloane, Is There a (72,36) d=16 Self-Dual Code?, IEEE Transactions on Information Theory 19(2) (1973), 251. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Introduces the existence question for an extremal doubly even self-dual code of length 72.Also cited at Sloane 1973, weight-distribution table and 5-(72,16,78) consequence; independently expanded and checked in etc72-artifact-enumerator-replay.
Cong Yu, Shixin Zhu, and Tingting Wu, New binary [72,36,12] self-dual codes from group rings and skew group rings, Computational and Applied Mathematics 44(1) (2025), Article 1. Cong Yu, Shixin Zhu, and Tingting Wu, New binary [72,36,12] self-dual codes from group rings and skew group rings, Computational and Applied Mathematics 44 (2025), construction results. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Constructs new self-dual length-72 codes of minimum distance 12 and gives no distance-16 witness.
Stefka Bouyuklieva, On the automorphisms of order 2 with fixed points for the extremal self-dual codes of length 24m, Designs, Codes and Cryptography 25(1) (2002), 5-13. Stefka Bouyuklieva, Designs, Codes and Cryptography 25 (2002), 5-13, exclusion of involutions with fixed points. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes fixed-point involutions from the automorphism group of a length-72 extremal code.
Stefka Bouyuklieva, On the automorphism group of a doubly-even (72,36,16) code, IEEE Transactions on Information Theory 50(3) (2004), 544-547. Stefka Bouyuklieva, IEEE Transactions on Information Theory 50(3) (2004), 544-547, exclusion of order-three automorphisms with fixed points. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes order-three automorphisms with fixed points from a length-72 extremal code.
Thomas Feulner and Gabriele Nebe, The automorphism group of an extremal [72,36,16] code does not contain Z7, Z3 x Z3, or D10, IEEE Transactions on Information Theory 58(11) (2012), 6916-6924. Thomas Feulner and Gabriele Nebe, IEEE Transactions on Information Theory 58(11) (2012), 6916-6924, exclusions of C7, C3 by C3, and D10. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes C7, C3 by C3, and D10 from the possible automorphism groups.
Martino Borello, The automorphism group of a self-dual [72,36,16] binary code does not contain elements of order 6, IEEE Transactions on Information Theory 58(12) (2012), 7240-7245. Martino Borello, IEEE Transactions on Information Theory 58(12) (2012), 7240-7245, exclusion of elements of order 6. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes automorphisms of order six from a length-72 extremal code.
Martino Borello, Francesca Dalla Volta, and Gabriele Nebe, The automorphism group of a self-dual [72,36,16] code does not contain S3, A4, or D8, Advances in Mathematics of Communications 7(4) (2013), 503-510. Martino Borello, Francesca Dalla Volta, and Gabriele Nebe, Advances in Mathematics of Communications 7(4) (2013), 503-510. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Excludes S3, A4, and D8 from the possible automorphism groups.
CC0 candidate record based on a primary paper and an independent Gleason-polynomial calculation.