Paper formalization status

Each paper below mirrors one source reference under Moore57/Papers/<paper>/. Statements marked Formalized have a Lean proof (explicit [done]/[wrap]/[external] marker, or a real proof body); Pending have a typed statement but no proof yet ([skeleton]/[deferred-heavy]/[GAP]); Out of scope are claims from the source paper that the Moore57 closures don’t need ([out-of-scope]).

Across all papers

1050 formalized · 13 pending · 26 out of scope · total 1089

Mačaj–Širáň 2010

Search for properties of the missing Moore graph. Linear Algebra Appl. 432 (2010), 2381–2398. DOI: 10.1016/j.laa.2009.07.018.

869 formalized · 13 pending · 0 out of scope · total 882 · section-by-section detail →

Aschbacher 1971

The Nonexistence of Rank Three Permutation Groups of Degree 3250 and Subdegree 57. J. Algebra 19 (1971), 538–540. DOI: 10.1016/0021-8693(71)90087-1.

23 formalized · 0 pending · 0 out of scope · total 23 · section-by-section detail →

Higman 1964

Finite permutation groups of rank 3. Math. Zeitschr. 86 (1964), 145–156. DOI: 10.1007/BF01111335.

92 formalized · 0 pending · 0 out of scope · total 92 · section-by-section detail →

Cameron, Permutation Groups, Ch. 3

Permutation Groups, Chapter 3 (Coherent configurations). Cambridge University Press, 1999. DOI: 10.1017/CBO9780511623677.004.

21 formalized · 0 pending · 26 out of scope · total 47 · section-by-section detail →

Makhnev–Paduchikh 2001

Automorphisms of Aschbacher Graphs. Algebra and Logic 40 (2) (2001), 69–74. DOI: 10.1023/A:1010217919915.

45 formalized · 0 pending · 0 out of scope · total 45 · section-by-section detail →