Research log — projective plane of order 12
Status (accessed 2026-08-17)
- Moorhouse, Projective Planes of Small Order — revised November 2017, re-fetched 2026-08-17. Catalogue of known planes of order . No order-12 incidence record. Completeness claimed only through order 10 (Lam–Kolesova–Thiel 1988; Lam–Thiel–Swiercz 1988). The empty slot is a database cross-check, not an exclusion.
- TheoremDB
projective-plane-order-12— snapshot 2026-07-25, records R592–R597. Existence still open. Strongest published symmetry: . - Wikipedia Projective plane, fetched 2026-08-17: order 12 still listed as open.
- Bruzda, arXiv:2607.25954 (2026): still the published lower bound; existence of six MOLS of order 12 remains open.
No later accepted construction or nonexistence theorem was found.
Published record we are measuring against
| claim | source | this folder |
|---|---|---|
| Bruck–Ryser silent at | Bruck–Ryser, Canad. J. Math. 1 (1949) | compute/replay_identities.py: ; |
| Bose–Chakravarti–Knuth, Technometrics 2 (1960) | not replayed (no BCK squares ingested); MacNeish gives 2, not 5 | |
| no elation of order 3 | Janko–van Trung, Stud. Sci. Math. 16 (1981) | cited, not re-proved |
| a -group, no , no nonabelian | Janko–van Trung 1980–82 | cited |
| divides 16 or 9 | Horvatić-Baldasar–Kramer–Matulić-Bedenić 1986–87 | cited |
| no | Suetake, JCTA 107 (2004) | cited |
| no | Akiyama–Suetake, JCD 16 (2008) | cited |
| no | Akiyama–Suetake–Tanaka, AJC 74 (2019) | local compute/refs/akiyama-suetake-tanaka-2019-order9.pdf |
| no ; hence | Akiyama–Suetake–Tanaka, JCD 31 (2023) | DOI 10.1002/jcd.21869; paywalled tonight, abstract + TheoremDB R595 |
| OA / 11-MOLS / Hadamard reformulation | Kharaghani–Suda, EJC 30 (2023) P2.49 | local compute/refs/kharaghani-suda-2023.pdf |
We did not beat the 2023 group-order classification. A dent tonight would have been a certified exclusion of one of the three remaining orders, or a construction.
Independent type arithmetic (this folder)
compute/classify_types.py (all checks pass, certs/type_classification.json):
- Unique order-2 Baer type: involutory elation ( even, not square; the involution ban is silent).
- No true homology of order 3: and .
- No generalized homology of order 3: axis action vs force incompatible conditions on the number of fixed points of the axis.
- No planar order-3 element with Fano Fix: an invariant ambient line would have 10 extra points.
- Remaining order-3 geometry: planar with , or generalized elation with . The elation is the 1981 theorem.
These divisibility lemmas recover the type list already used in the 2009/2019 Akiyama–Suetake papers. They are not claimed as a new forbidden automorphism type.
Computational residue on
An involutory elation is equivalent to MOLS of order 12 with . Already would be implied.
| instance | result | certificate |
|---|---|---|
| involution-Latin | SAT | certs/t1_squares.json, independent verifier |
| (SAT search) | SAT | certs/t2_squares.json |
| MacNeish product | explicit | certs/macneish_involution_2mols.json |
| third mate of the SAT pair | UNSAT | certs/mate_t2.drat, drat-trim VERIFIED |
| third mate of MacNeish | UNSAT | certs/mate_macneish.drat, drat-trim VERIFIED |
| cell-symbol | UNKNOWN at 2400s | certs/t3c.out: 45,210,387 conflicts, 2396s |
| UNKNOWN at 2400s | certs/sd3.out: 21,232,051 conflicts, 2396s |
The two mate-UNSAT proofs show that two distinct isotopy classes of involution 2-MOLS are maximal. They do not classify all classes. Search residue is not a bound.
Sources fetched tonight
- https://ericmoorhouse.org/pub/planes/
- https://www.theoremdb.org/statements/projective-plane-order-12/
- https://www.theoremdb.org/records/pp12-attempt-literature-and-catalogue-audit
- https://ajc.maths.uq.edu.au/pdf/74/ajc_v74_p112.pdf
- https://ajc.maths.uq.edu.au/pdf/43/ajc_v43_p133.pdf
- https://arxiv.org/pdf/2211.02410 (Kharaghani–Suda)
- https://mathoverflow.net/questions/38632/projective-plane-of-order-12
- https://doi.org/10.1002/jcd.21869 (abstract only)