Moore (57, 2) — automorphism group tracker

Whether a Moore graph Γ of degree 57 and diameter 2 exists is a long-standing open question. If it does, its automorphism group G = Aut(Γ) has a finite order. By results of Aschbacher, Higman, Makhnev–Paduchikh, and Macaj–Siran (2010), |G| divides one of 13 maxima — and therefore takes one of 35 candidate values (the union of divisors of those 13 maxima). For each candidate order d there are a(d) finite groups up to isomorphism (OEIS A000001), giving 107 candidate groups in total.

Within the 35-order candidate space, Macaj–Siran (2010) — combined with the cited Makhnev–Paduchikh (2001) Theorem — already excludes 26 specific groups at the group level (not just constrains orbits): notably cyclic Z₄₉ at order 49 (Lemma 19); D₁₁, Z₃₈, Z₁₁₀ and many large-|Y| dihedral-like groups at orders 18, 22, 38, 50, 54, 110, 147 via Theorem 2's structural restriction |Y| ∈ {1, 3, 5, 7, 19, 21, 57} and §9's "no element of order 110" remark; plus the 3 groups of order 375 whose Sylow-5 is ℤ₅³ or non-abelian, ruled out by Theorem 5 / Proposition 4. That leaves 81 paper-allowed candidate groups.

This project closes three full orders — 22, 38, 110 — at the group level (10 of the 107 groups), and the 4 of those 10 that the paper had not excluded are the original contribution here: Z₂₂ (order 22), D₁₉ (order 38), and the two groups at order 110 outside the paper's reach (D₅ × Z₁₁, Z₂ × (Z₁₁ ⋊ Z₅)). All ten are formally verified in Lean.

Beyond the three full-order closures, this project also Lean-excludes seven cyclic-only groups at seven odd orders that the paper does not address: C₂₁, C₃₉, C₅₇, C₇₅, C₁₇₁, C₂₇₅, C₃₇₅ (the cyclic generator at each order). Six use an elementary orbit-count / mod-arithmetic argument; the last (C₂₁) uses the Petersen-centralizer + Aut(Petersen) ≅ S₅ (no order 7 in S₅) infrastructure built on the A'.4 track (proofs/no_cyclic_aut_groups_moore57.md). Together, that is 17 Lean-certified group exclusions (11 of them project-original). This site tracks two distinct layers of work:

1. Natural-language proofs that close each group-order case mathematically (proofs/no_aut_order_22_moore57.md, proofs/moore57_d19_lean_aware_proof.md, proofs/no_cyclic_aut_groups_moore57.md), extending the Macaj–Siran framework.
2. Lean 4 / Mathlib formalization of those proofs, verified against an explicit axiom allowlist (AxiomsCheck.lean).

Closing further candidates needs both layers: a human proof and its mechanical certificate. See Contribute for entry points.

Denominators: 35 = candidate orders = union of divisors of the 13 Macaj–Siran maxima (25 odd via Theorem 6, 10 even via Theorem 7). 107 = total finite groups across those 35 orders (65 odd + 42 even), OEIS A000001. 81 = paper-allowed candidate groups (107 − 26 paper-excluded). Max remaining: |G| ≤ 375 (odd, unchanged from paper); |G| ≤ 54 (even, down from 110 after this project closed orders 22, 38, 110).

At a glance — 35 candidate orders

Each tile is a candidate value of |G|: the 13 Macaj–Siran (2010) maxima together with their proper divisors (which inherit the maxima's constraints). The Theorem 6 / 7 tables below show which maxima each order divides. Click for full group classification and paper context.

Odd candidates (25 orders, 65 groups, 7 cyclic Lean-excluded)

Even candidates (10 orders, 42 groups, 10 excluded)

Theorem 6 (odd case) — full candidate list

Macaj–Siran, 2010, Theorem 6. Let Γ be a Moore graph of degree 57 on 3250 vertices and G = Aut(Γ). If |G| is odd then |G| divides one of 35, 39, 135, 147, 171, 275, 375 — and therefore |G| equals one of the 25 odd divisors below.

Theorem 7 (even case) — full candidate list

Macaj–Siran, 2010, Theorem 7. If |G| is even then |G| divides one of 14, 22, 38, 50, 54, 110. Note 4 ∤ |G| (Lemma 2; Higman / Cameron), so even divisors take one of the 10 values below.

Paper formalization status

Beyond the group-order tracker above, each of the 5 reference papers has its own Lean-mirroring directory under Moore57/Papers/<paper>/. Below is the rolled-up statement-level status; see Papers for the §-level drill-down.

Reference

M. Macaj and 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.

See also About for the full reference list and notes on the Lean formalization.