Contribute

Join the open formalization of automorphism-group restrictions for the hypothetical Moore (57, 2) graph.

Why participate?

Whether a Moore graph of degree 57 and diameter 2 exists is a long-standing open problem in algebraic combinatorics. Each entry on the tracker is a concrete piece of that puzzle: a candidate group / order that, if ruled out, narrows the structure of any hypothetical Aut(Γ) — or eventually shows Aut(Γ) must be trivial.

This project is doing original mathematics, not just formalization. The Macaj–Siran 2010 paper provides the candidate list and partial constraints, but the full exclusion of a group order (as opposed to an element order) is in most cases not in any published paper. Three orders (22, 38, 110) have already been closed both mathematically and formally. Beyond those full-order closures, this project has also Lean-excluded seven cyclic generator cases at odd orders. After these results, 90 finite groups across 32 candidate orders remain Lean-open.

Two layers, both contributions

Closing a new candidate involves two distinct kinds of work, and each is independently a contribution (see the methodology):

  1. Layer 2 — Natural-language proof. A careful mathematical writeup that closes the group-order case (or a sub-group case such as the cyclic generator), built on top of the Macaj–Siran framework. Existing examples: proofs/no_aut_order_22_moore57.md, proofs/moore57_d19_lean_aware_proof.md, and the cyclic-narrowing note proofs/no_cyclic_aut_groups_moore57.md (7 cyclic orders: C₂₁, C₃₉, …, C₃₇₅).
  2. Layer 3 — Lean formalization. A machine-checked Lean 4 / Mathlib proof that elaborates against the axiom allowlist in AxiomsCheck.lean.

You do not have to do both. A clean Layer-2 writeup unlocks Layer-3 work for someone else, and a Layer-3 attempt often shakes loose Layer-2 ambiguities. Either is valuable.

Ways to help

SkillLayerWhat to do
Original natural-language proof Layer 2 Pick an open order and write a complete proof in proofs/no_aut_order_N_moore57.md style. The paper's Lemma 12 / 13 / 14 / 15 tables provide partial constraints; your contribution combines them into a full group-order exclusion. This is the highest-leverage mathematical contribution — most open candidates are waiting for this.
Lean 4 / Mathlib Layer 3 Take an existing natural-language proof (Layer 2) and formalise it in Lean. Templates: the Moore57/Order22OnMoore57/ and Moore57/C38OnMoore57/ modules for full-order closures, or Moore57Graph/Aut/CyclicGroupExclusions.lean for elementary cyclic narrowing. Must pass AxiomsCheck.lean.
Math review Layer 2 / 3 Cross-check the Layer-2 writeups in proofs/ against the original Macaj–Siran arguments, and the Lean formalisations in Moore57/ against the Layer-2 writeups.
Finite-group theory Layer 2 Refine the SmallGroup tables on the per-order pages (GAP IDs, conjugacy of semidirect products, action lattice on Sylow subgroups). Especially needed for orders 54, 135, 147, 375.
GAP / SageMath Layer 2 Build supporting computations (orbit structures, character tables of candidate subgroups, equitable partitions) that inform or replace ad-hoc case analysis in the natural-language and Lean proofs.
Writing / outreach Meta Blog notes (see blogs/), arxiv preprints, or talks. We are particularly interested in producing a self-contained writeup of the D₁₉ proof for arXiv submission.

Pick a target

All Lean-open orders are listed on the top page. A rough "approachability" ranking based on the existing infrastructure:

14 2 · 7 0 / 2 open closest analogue of order 22 50 2 · 5² 0 / 5 open order-25 Sylow + involution 35 5 · 7 0 / 1 open single group, Lemma 15 starred row 39 3 · 13 1 / 2 excluded Lemma 12 row for p = 13 54 2 · 3³ 0 / 15 open 15 groups but Theorem 4 bound helps 375 3 · 5³ 1 / 4 excluded hardest; GAP-aided in the paper

"Open" here means no Lean proof of no_OrderN_acts_on_Moore57 exists yet. Orders such as 39, 171, 275, and 375 already have a cyclic generator excluded in Lean, but their remaining non-cyclic group cases are still fair game.

Getting started (Lean)

Prerequisites: a working Lean 4 / Mathlib setup (Lean 4.x + elan). Then: 

git clone https://github.com/yawara/moore57.git
cd moore57
lake build

Build is large (≈ 4000 jobs) and takes 30–60 minutes from scratch. Subsequent rebuilds are incremental. Key entry points:

CI will reject any sorry or admit in proof position. The axiom allowlist is enforced at build time.

Communication

Recognition

Contributions are credited via Co-Authored-By on commits, mention in the corresponding blog entry, and (where appropriate) authorship on any arxiv writeup that emerges from this work. The project is MIT-licensed; you retain the credit for any proof you contribute.