Blocking sets of PG(2,13) invariant under a fixed-point-free Singer subgroup meet some line in five points

Statement and scope

Formal scope. Lean 4.35.0 models PG(2,13) with Mathlib's projectivization of F₁₃³ and proves that the Singer cycle has order 183, that its subgroup H of order three fixes no point, that the 21-point witness is an H-invariant minimal blocking set with largest line intersection five, the reduction of every H-invariant set to 61 orbit conditions, and the nonexistence of a solution with intersections at most four, by a kernel-checked search with a soundness proof; the main theorem is IsLeast admissibleCaps 5. The conjugacy of all fixed-point-free subgroups of order three is conventional.

Lean 4.35.0 models PG(2,13) with Mathlib's projectivization of F₁₃³ and proves the order of the Singer cycle, the fixed-point-free subgroup, the 21-point witness, the reduction to 61 orbit conditions and the nonexistence of a solution with intersections at most four, by a kernel-checked search with a soundness proof. The conjugacy of all fixed-point-free subgroups of order three is conventional.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site

manuscript.pdf 309 KB

PDF on GitHub

papers/mathematics/singer-orbit-blocking/manuscript.pdf

LaTeX source

papers/mathematics/singer-orbit-blocking/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/singer-orbit-blocking/

Lean project

papers/mathematics/singer-orbit-blocking/lean/ 27 Lean files

Lakefile

papers/mathematics/singer-orbit-blocking/lean/lakefile.toml

Toolchain

leanprover/lean4:v4.35.0

Library roots

• lean/SingerC3.lean
• lean/SingerC3/

Reproduce

The commands below are quoted from papers/mathematics/singer-orbit-blocking/VERIFICATION.md, which gives their context and working directory.

python3 verify.py --output /tmp/singer-orbit-blocking-verification

README

papers/mathematics/singer-orbit-blocking/README.md

Verification guide

papers/mathematics/singer-orbit-blocking/verification/README.md

Verification record

papers/mathematics/singer-orbit-blocking/VERIFICATION.md

Authorship

papers/mathematics/singer-orbit-blocking/AUTHORSHIP.md

Repository guide

verification/README.md

Unfinished proofs

UNFINISHED.md

Source and prior work

Prior work. Erdős Problem #1159. · Blokhuis, Brouwer and Wilbrink, 2003.

Source. Erdős Problem 1159 asks whether every finite projective plane has a point set meeting each line in between one and C points; Erdős, Silverman and Stein (1983) proved an O(log n) bound. The 21-point example is due to Blokhuis, Brouwer and Wilbrink (Adv. Geom. 2003, Section 5.3), and a public campaign log recorded this Singer-orbit case for q = 13 as unresolved. Historical priority is not certified.

Questions and answers

What is the least largest line intersection of a Singer-invariant blocking set in PG(2,13)?

Five. Let H be the subgroup of order three of a Singer cycle group of PG(2,13), which fixes no point. Every H-invariant blocking set meets some line in at least five points, and the 21-point blocking set of Blokhuis, Brouwer and Wilbrink, which is invariant under a conjugate of H, meets every line in at most five points. Every fixed-point-free collineation of order three generates a conjugate of H, so the answer is the same for all of them.

Does this answer Erdős Problem 1159 for the plane of order 13?

No. It settles only blocking sets with this symmetry. Whether PG(2,13) has a blocking set meeting every line in at most four points, with no symmetry assumed, is not decided here, and the general problem for all finite projective planes remains open.

How is the result verified?

The question reduces to 61 weighted line conditions on the orbits of H. A Lean 4 project proves the whole theorem for the specified subgroup, with PG(2,13) modelled by Mathlib's projectivization of F₁₃³; the exhaustive search runs in the Lean kernel with a soundness proof, without native_decide. An independent Python program repeats the geometry, the witness checks and the search. The conjugacy of all fixed-point-free subgroups of order three has a conventional proof. Historical priority is not certified.

Cite

Citation file papers/mathematics/singer-orbit-blocking/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026singerorbitblocking,
  author = {Goyal, Dev D.},
  title = {Blocking Sets of {PG}(2,13) Invariant under a Fixed-Point-Free {Singer} Subgroup Meet Some Line in Five Points},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/singer-orbit-blocking}
}

Copy BibTeX