About

What is the Moore (57, 2) graph?

A Moore graph of degree d and diameter k is a connected regular graph of degree d, diameter k, and order attaining the Moore bound. By Hoffman–Singleton (1960) and Damerell / Bannai–Ito (1973), Moore graphs of diameter 2 can only have degrees d ∈ {2, 3, 7, 57}; the first three exist uniquely (C₅, Petersen, Hoffman–Singleton), while the case d = 57 remains open.

Such a graph would have 3250 vertices, girth 5, and would be a strongly regular graph SRG(3250, 57, 0, 1).

Why automorphism orders?

A series of papers (Aschbacher 1971, Higman, Cameron, Makhnev–Paduchikh 2001, Macaj–Siran 2010) progressively narrowed the possible values of |Aut(Γ)|. The strongest published bounds are summarised in the two theorems of Macaj–Siran 2010 reproduced on the top page:

• Odd case: |G| ≤ 375, divides one of 7 numbers.
• Even case: |G| ≤ 110, divides one of 6 numbers.

Excluding more of these candidates would strengthen our understanding of any hypothetical Γ. Reducing the list to |G| = 1 would say the graph (if it exists) is asymmetric.

Methodology — three layers

This project sits between the published paper and machine verification. Each closed candidate involves three distinct kinds of work:

1. Paper layer (Macaj–Siran 2010 et al.): establishes the candidate list (13 maxima) and partial constraints — Lemma 12 tables of (a₀, a₁, χ₁) for prime-order elements, Lemma 13 for p², Lemma 15 starred rows for products pq, the Higman trace identity, and Theorems 4–7 on p-group bounds and the odd / even split.
2. Natural-language proof layer (this project): extends the paper's framework — either to fully exclude a group order (e.g. 22, 38, 110) or to partially narrow it (cyclic subgroup at a paper-allowed order). For 22 and 38 the paper only lists them as candidates; for 110 it only excludes elements of that order. The new proofs combine the paper's tools with extra ingredients (F₁₁ permutation module, character restrictions, Sylow + Cauchy subgroup extraction, elementary cyclic orbit-counts) into complete arguments. The writeups live in proofs/.
3. Lean 4 / Mathlib formalization layer (this project): a machine-checked encoding of the layer-2 proofs. Each main theorem is asserted to depend only on propext + Classical.choice + Quot.sound (and a few compiler-generated native_decide axioms) by the AxiomsCheck.lean gate, which is enforced at build time.

Closing a new candidate therefore needs both layers 2 and 3 (the paper layer is shared infrastructure). Either layer alone is a meaningful contribution — see Contribute for entry points.

Lean formalization status

The companion repository github.com/yawara/moore57 contains Lean 4 / Mathlib formalizations. Three full orders are unconditionally excluded at the group level:

A further seven cyclic-only group exclusions at seven odd orders are also Lean-certified. Six share an elementary orbit-count / mod-arithmetic kernel (Foundations/GroupAction/CyclicOrbitCount.lean); the seventh (C₂₁) uses the Petersen-centralizer argument and the project's own Aut(Petersen) ≅ S₅ chain built on the A'.4 track:

All seven are in Moore57/Moore57Graph/Aut/CyclicGroupExclusions.lean; none was paper-excluded. The natural-language writeup of all seven cyclic exclusions (with refinements and the larger cyclic-status table) is at proofs/no_cyclic_aut_groups_moore57.md.

Each Lean closure is checked by Moore57/AxiomsCheck.lean against an explicit allowlist of axioms (propext, Classical.choice, Quot.sound, and compiler-generated native_decide axioms).

References

1. M. Aschbacher, The nonexistence of rank three permutation groups of degree 3250 and subdegree 57, J. Algebra 19 (1971), 538–540.
2. E. Bannai, T. Ito, On finite Moore graphs, J. Fac. Sci. Univ. Tokyo Sect. I A 20 (1973), 191–208.
3. P. J. Cameron, Permutation Groups, Cambridge University Press, 1999.
4. R. M. Damerell, On Moore graphs, Math. Proc. Cambridge Philos. Soc. 74 (1973), 227–236.
5. A. J. Hoffman, R. R. Singleton, On Moore graphs with diameters 2 and 3, IBM J. Res. Develop. 4 (1960), 497–504.
6. A. A. Makhnev, D. V. Paduchikh, Automorphisms of Aschbacher Graphs, Algebra Logic 40 (2001), 69–74. DOI: 10.1023/A:1010217919915.
7. M. Macaj, J. Siran, Search for properties of the missing Moore graph, Linear Algebra Appl. 432 (2010), 2381–2398. DOI: 10.1016/j.laa.2009.07.018.
8. M. Miller, J. Siran, Moore graphs and beyond: a survey of the degree/diameter problem, Electron. J. Combin., Dynamic Survey DS14 (2005).
9. C. Dalfo, A survey on the missing Moore graph, Linear Algebra Appl. 569 (2019), 1–14. DOI: 10.1016/j.laa.2018.12.035.

Site and source

This site is static HTML hosted out of the docs/ directory of the moore57 repository. Styling is provided by Pico CSS v2; all content reflects published mathematics, and any errors are the maintainer's.