Remark 1. A projective plane of order 12 has 157 points and 157 lines.
Remark 2. Every line contains 13 points, every point lies on 13 lines, and each pair of points lies on exactly one line.
2What counts as a solution
Supply a 157 by 157 incidence matrix satisfying the plane axioms, or give a complete nonexistence proof with independently replayable case certificates.
Current status (Existence at order 12 remains open). The literature and catalogue audit found no accepted construction or complete exclusion for a projective plane of order 12.[1][2][4]
1Packet records
6 records
Record
Kind
Assessment
The literature and catalogue audit found no accepted construction or complete exclusion for a projective plane of order 12.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Proposition 1
The literature and catalogue audit found no accepted construction or complete exclusion for a projective plane of order 12.[1][2][4]
Relevance to this problem
For A projective plane of order 12, record pp12-claim-open-status (“Existence at order 12 remains open”) records a bound, answer, status fact, or structural consequence. The record states: The literature and catalogue audit found no accepted construction or complete exclusion for a projective plane of order 12.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
open
Scope
existence of a finite projective plane of order 12, equivalently a symmetric 2-(157,13,1) design
A projective plane of order 12 would have 157 points and 157 lines. Every line would contain 13 points, every point would lie on 13 lines, and each pair of points would determine one line. Equivalently, it would be a symmetric \(2\text{-}(157,13,1)\) design.
Akiyama, Suetake, and Tanaka state in their 2019 primary paper that the order-12 existence question is still unknown. Their exhaustive computation excludes collineation groups of order 9. Their 2023 sequel sharpens the symmetry restriction to collineation-group orders 1, 2, or 3 while leaving the plane itself unresolved. Kharaghani and Suda give a 2023 equivalence with a balancedly multi-splittable quaternary Hadamard matrix of order 144, which supplies another exact target rather than a resolution.
The research check through 2026-07-25 found no later accepted construction or nonexistence theorem. The answer recorded here is therefore open.
The theorem's sum-of-two-squares condition applies to orders congruent to 1 or 2 modulo 4, while 12 is congruent to 0.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1
The theorem's sum-of-two-squares condition applies to orders congruent to 1 or 2 modulo 4, while 12 is congruent to 0.[5]
Relevance to this problem
For A projective plane of order 12, record pp12-claim-bruck-ryser-silent (“Bruck-Ryser gives no obstruction at order 12”) records a bound, answer, status fact, or structural consequence. The record states: The theorem's sum-of-two-squares condition applies to orders congruent to 1 or 2 modulo 4, while 12 is congruent to 0.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
established
Scope
the projective-plane form of the Bruck-Ryser theorem and the incidence determinant identity at order 12
Bruck and Ryser prove that if a projective plane of order \(n\) exists and \(n\equiv1\) or \(2\pmod4\), then \(n\) must be a sum of two integer squares. Since
\[
12\equiv0\pmod4,
\]
the theorem is silent here.
The elementary determinant condition is also consistent. If \(B\) is a \(157\times157\) incidence matrix, then
\[
BB^{\mathsf T}=12I_{157}+J_{157}.
\]
The eigenvalues on the right are \(169=13^2\) once and 12 with multiplicity 156. Hence
\[
\det(B)^2=13^2\,12^{156}
\quad\text{and}\quad
|\det(B)|=13\,12^{78}.
\]
This is an integer square identity, so it supplies no contradiction. Any order-12 exclusion needs information beyond this arithmetic test.
The strongest published symmetry restriction leaves only trivial, involutory, or order-three collineation groups.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Proposition 2
The strongest published symmetry restriction leaves only trivial, involutory, or order-three collineation groups.[2][1]
Relevance to this problem
For A projective plane of order 12, record pp12-claim-collineation-orders (“Every collineation group has order 1, 2, or 3”) records a bound, answer, status fact, or structural consequence. The record states: The strongest published symmetry restriction leaves only trivial, involutory, or order-three collineation groups.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
established
Scope
the full class of projective planes of order 12 and every collineation group acting on any such plane
Akiyama, Suetake, and Tanaka prove that a projective plane of order 12 cannot admit a collineation group of order 4. Their paper combines this result with the earlier exclusions and states the resulting classification:
\[
|G|\in\{1,2,3\}
\]
for every collineation group \(G\) of a hypothetical plane of order 12. In particular, its full collineation group would have one of these three orders.
This theorem sharply limits symmetry-based enumeration. A search restricted to automorphism groups of order at least 4 covers an empty class. A complete computation must still handle planes with a trivial group or a group of order 2 or 3.
A 1960 construction proves N(12) at least 5; the universal upper bound is 11, and equality is equivalent to an order-12 plane.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Proposition 3
A 1960 construction proves N(12) at least 5; the universal upper bound is 11, and equality is equivalent to an order-12 plane.[3]
Relevance to this problem
For A projective plane of order 12, record pp12-claim-five-mols-lower-bound (“Five order-12 MOLS are constructed, while eleven would settle the problem”) records a bound, answer, status fact, or structural consequence. The record states: A 1960 construction proves N(12) at least 5; the universal upper bound is 11, and equality is equivalent to an order-12 plane.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
established
Scope
the maximum number N(12) of pairwise mutually orthogonal Latin squares of order 12
Let \(N(12)\) be the largest size of a pairwise mutually orthogonal family of Latin squares of order 12. Bose, Chakravarti, and Knuth explicitly construct two families of five in their 1960 paper, proving
\[
N(12)\ge5.
\]
The universal bound gives \(N(12)\le11\). A family of 11 is a complete family, equivalent to an affine plane and hence to a projective plane of order 12.
Thus the published five-square construction supplies a concrete partial object. Extending any compatible family to 11 would prove existence. A proof that all complete-family branches fail would prove nonexistence.
The audit located strong arithmetic and symmetry restrictions, a five-MOLS construction, and exact reformulations, while the existence question stayed open.
Trace
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
attempt · Route 1
The audit located strong arithmetic and symmetry restrictions, a five-MOLS construction, and exact reformulations, while the existence question stayed open.[6][5][3][1][2][4]
Relevance to this problem
For A projective plane of order 12, record pp12-attempt-literature-and-catalogue-audit (“Primary literature and small-plane catalogue audit”) documents a concrete method, search boundary, or failed route. The record states: The audit located strong arithmetic and symmetry restrictions, a five-MOLS construction, and exact reformulations, while the existence question stayed open.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
The audit checked the 1949 Bruck-Ryser paper, the 1960 five-MOLS construction, the 2019 order-9 collineation exclusion, the 2023 order-4 exclusion, and the 2023 Hadamard equivalence. It also checked Eric Moorhouse's Projective Planes of Small Order catalogue, which describes itself as a current list of known small planes and includes every known plane below order 34 known to its maintainer. The table has no order-12 incidence record.
The catalogue states that its completeness guarantee ends at order 10. Its empty order-12 slot therefore serves as a database cross-check rather than a mathematical exclusion. The strongest global restriction found is the 2023 theorem that every collineation group has order 1, 2, or 3. The strongest explicit partial Latin-square object found remains a family of five MOLS. The complete family of 11 remains unconstructed.
A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.[4]
Relevance to this problem
For A projective plane of order 12, record pp12-artifact-model-audit (“Exact OA and 11-MOLS computational formulation”) supplies evidence or a replay used to check the packet. The record states: A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
parameter arithmetic and the complete constraint inventory for an 11-MOLS constraint-programming formulation at order 12
join source_lines with newline and run with python3
Runtime
CPython 3, standard library only
Details
Use integer variables
\[
L_{k,r,c}\in\{0,\ldots,11\},
\quad 0\le k<11,\quad0\le r,c<12.
\]
For each \(k\), impose `AllDifferent` on every row and every column of \(L_k\). This gives 264 Latin constraints. For each pair \(k<\ell\), impose `AllDifferent` on the 144 values
\[
12L_{k,r,c}+L_{\ell,r,c}.
\]
There are 55 such constraints. Since every encoded value lies between 0 and 143, each constraint forces every ordered symbol pair to occur once. A satisfying assignment is exactly a complete family of 11 MOLS, or equivalently an \(OA_1(144,13,12,2)\).
Safe normalization fixes \(L_{k,0,c}=c\) for every \(k,c\), then fixes \(L_{0,r,0}=r\) for \(1\le r<12\). These are 143 fixed cells. They come from row and column permutations plus independent symbol relabeling. Any satisfying assignment constructs the plane. A complete unsatisfiability certificate for this normalized model proves nonexistence.
The inline program checks the design identities, the determinant value, the orthogonal-array dimensions, and the full constraint inventory. Its canonical report has SHA-256 digest `c980fe81ebe7fa46510d87f9c4c8f000f681b13eaff128ebb54bdfab7797feb1`.
The parameters make this a sharply bounded design search. A full solution is formidable, while smaller symmetry classes and failed canonical augmentations are reusable units of evidence.
Original intake status. Status remains unverified. The order-12 existence question has a long literature, so a current finite-geometry bibliography check belongs before a large search.
Encode one line and its pencil in canonical form, then use exact cover for the remaining point pairs. Record canonical augmentation rules and automorphism-group assumptions with every exclusion.
Trap: the Bruck-Ryser-Chowla obstruction has no force at order 12 because 12 is divisible by 4. Reusing that test as an exclusion silently proves nothing here.
Recorded example 1. The incidence matrix B would satisfy BB^T=12I+J and every row and column would have weight 13.
Computational notes
Exact parameter checks give b=v=12^2+12+1=157, block size 13, replication 13, and 157 choose 2 = 12246 point pairs, matching 157 times 13 choose 2. The determinant identity det(B)^2=13^2 times 12^156 passes the elementary square test, so this route supplies no contradiction.
How the 6 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“A projective plane of order 12.” TheoremDB. P2614. Problem statement; statement text SHA-256 a650bc8b9cccd698a4971e760c61e31d3ae29e5678491854b69a42f3083bb20a. https://theoremdb.org/statement/?ref=P2614
BibTeX
@misc{theoremdb-problem-a650bc8b9cccd698a4971e760c61e31d3ae29e5678491854b69a42f3083bb20a,
title = {{A projective plane of order 12}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 a650bc8b9cccd698a4971e760c61e31d3ae29e5678491854b69a42f3083bb20a},
url = {https://theoremdb.org/statement/?ref=P2614}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
Kenzi Akiyama, Chihiro Suetake, and Masaki Tanaka, The nonexistence of projective planes of order 12 with a collineation group of order 9, Australasian Journal of Combinatorics 74(1) (2019), 112-160. Main theorem and corollary on pp. 112-114. ↗journal article · primary source · version of record · checked 2026-07-25Source use: citation only.For A projective plane of order 12: The literature and catalogue audit found no accepted construction or complete exclusion for a projective plane of order 12.Also cited at Akiyama, Suetake, and Tanaka, Australasian Journal of Combinatorics 74(1) (2019), 112-160, pages 112-114.Also cited at Akiyama, Suetake, and Tanaka, Australasian Journal of Combinatorics 74(1) (2019), main theorem.Also cited at Kenzi Akiyama, Chihiro Suetake, and Masaki Tanaka, The nonexistence of projective planes of order 12 with a collineation group of order 9, Australasian Journal of Combinatorics 74(1) (2019), 112-160, Introduction and main theorem; status cross-checked against the 2023 sources listed in metadata.order-9 exclusion and 2019 open-status statement
Packet source. Kenzi Akiyama, Chihiro Suetake, and Masaki Tanaka, Projective planes of order 12 do not have a collineation group of order 4, Journal of Combinatorial Designs 31(2) (2023), 87-123. Abstract and main theorem. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.For A projective plane of order 12: The strongest published symmetry restriction leaves only trivial, involutory, or order-three collineation groups.Also cited at Akiyama, Suetake, and Tanaka, Journal of Combinatorial Designs 31(2) (2023), abstract and main theorem.Also cited at Kenzi Akiyama, Chihiro Suetake, and Masaki Tanaka, Projective planes of order 12 do not have a collineation group of order 4, Journal of Combinatorial Designs 31(2) (2023), 87-123, abstract and main theorem.all collineation-group orders reduced to 1, 2, or 3Source named by the research packet.
R. C. Bose, I. M. Chakravarti, and D. E. Knuth, On Methods of Constructing Sets of Mutually Orthogonal Latin Squares Using a Computer. I, Technometrics 2(4) (1960), 507-516. R. C. Bose, I. M. Chakravarti, and D. E. Knuth, On Methods of Constructing Sets of Mutually Orthogonal Latin Squares Using a Computer. I, Technometrics 2(4) (1960), 507-516, abstract, Figure 1, and Table 2. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.For A projective plane of order 12: A 1960 construction proves N(12) at least 5; the universal upper bound is 11, and equality is equivalent to an order-12 plane.two explicit sets of five MOLS of order 12
Hadi Kharaghani and Sho Suda, Hadamard Matrices related to Projective Planes, Electronic Journal of Combinatorics 30(2) (2023). The projective-plane, orthogonal-array, and complete-MOLS equivalences are standard and are used in Kharaghani and Suda, Electronic Journal of Combinatorics 30(2) (2023), P2.49; exact parameter audit executed 2026-07-25. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.For A projective plane of order 12: A 1,584-variable finite-domain model is equivalent to the required orthogonal array and has safe first-row and first-column symmetry breaking.Also cited at Hadi Kharaghani and Sho Suda, Hadamard Matrices related to Projective Planes, Electronic Journal of Combinatorics 30(2) (2023), P2.49, main equivalence.equivalence with a balancedly multi-splittable quaternary Hadamard matrix of order 144
R. H. Bruck and H. J. Ryser, The Nonexistence of Certain Finite Projective Planes, Canadian Journal of Mathematics 1(1) (1949), 88-93. R. H. Bruck and H. J. Ryser, The Nonexistence of Certain Finite Projective Planes, Canadian Journal of Mathematics 1 (1949), 88-93, Theorem 1; order-12 substitution and determinant calculation replayed in pp12-artifact-model-audit. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.For A projective plane of order 12: The theorem's sum-of-two-squares condition applies to orders congruent to 1 or 2 modulo 4, while 12 is congruent to 0.Bruck-Ryser necessary condition
Eric Moorhouse, Projective Planes of Small Order, author-maintained catalogue (revised November 2017). Catalogue description and the order-12 table entry. ↗website · reference source · web version checked 2026-08-01 · checked 2026-07-25Source use: citation only.Records the known small projective planes and leaves order 12 unresolved.Also cited at Eric Moorhouse, Projective Planes of Small Order, catalogue description and order table, accessed 2026-07-25; primary sources listed in metadata.For A projective plane of order 12: The audit located strong arithmetic and symmetry restrictions, a five-MOLS construction, and exact reformulations, while the existence question stayed open.
CC0 problem record with independently checked design parameters.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.