Prove2Me

Every Steiner triple system on 77 points is the Fano plane

Proved
FanoUnique.sts7_is_fano

by ShapeZero · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfano-planesteiner-triple-systems

Let SS be any Steiner triple system on {0,…,6}\{0, \dots, 6\}: a family of 33-point lines such that every pair of distinct points lies on exactly one line. Then SS is the Fano plane up to relabelling: there is a permutation ee of {0,…,6}\{0, \dots, 6\} with

{ e(ℓ):ℓ a line of S }={{i, i+1, i+3}:i∈Z/7}.\{\, e(\ell) : \ell \text{ a line of } S \,\} = \bigl\{\{i,\ i+1,\ i+3\} : i \in \mathbb{Z}/7\bigr\}.

This is the uniqueness of STS(7), which C1 §3 cites as classical.

Preamble
import Mathlib
import Definitions.Def_FanoUnique_isFano
Formal statement
namespace FanoUnique

open RolesForceSeven

theorem sts7_is_fano (S : STS 7) : IsFano S := by
  sorry

end FanoUnique
Source
Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3, Theorem 3.3 ("hence the unique STS(7) (the Fano plane PG(2, 2))") and its proof ("Uniqueness of STS(7) is classical"): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; public references: Wikipedia, "Fano plane": https://en.wikipedia.org/wiki/Fano_plane ; Wikipedia, "Steiner system": https://en.wikipedia.org/wiki/Steiner_system
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Theorem (sts7_is_fano). Let [7]={0,1,…,6}[7] = \{0,1,\dots,6\} denote the type of natural numbers below 77, with addition taken modulo 77. The theorem takes a single explicit argument SS, a Steiner triple system on 7 points in the following sense. An object SS of this kind consists of

  • a finite collection L(S)\mathcal{L}(S) of subsets of [7][7] (the "lines"), together with the two properties
  • every line ℓ∈L(S)\ell \in \mathcal{L}(S) has exactly 33 elements, and
  • for all points x,y∈[7]x, y \in [7] with x≠yx \neq y there is exactly one ℓ\ell with ℓ∈L(S)\ell \in \mathcal{L}(S), x∈ℓx \in \ell and y∈ℓy \in \ell.

No other conditions are imposed. In particular, nothing is assumed about how many lines there are or about which point sets occur, apart from what these two properties force. The hypotheses can be satisfied: the reference system F\mathcal{F} below is one example.

The reference Fano system F\mathcal{F} has line set

L(F)={ {i,  i+1,  i+3}  :  i∈[7] }(arithmetic mod 7),\mathcal{L}(\mathcal{F}) = \{\, \{i,\; i+1,\; i+3\} \;:\; i \in [7] \,\} \quad (\text{arithmetic mod } 7),

which works out to the seven triples

{0,1,3}, {1,2,4}, {2,3,5}, {3,4,6}, {4,5,0}, {5,6,1}, {6,0,2}.\{0,1,3\},\ \{1,2,4\},\ \{2,3,5\},\ \{3,4,6\},\ \{4,5,0\},\ \{5,6,1\},\ \{6,0,2\}.

Only this line set is used in the statement.

Conclusion. SS is "Fano": there exists a bijection e:[7]→[7]e : [7] \to [7] (a permutation of the 77 points) such that applying ee pointwise to every line of SS gives exactly the Fano lines, as an equality of sets of lines:

{ e(ℓ):ℓ∈L(S) }  =  L(F),e(ℓ)={e(x):x∈ℓ}.\{\, e(\ell) : \ell \in \mathcal{L}(S) \,\} \;=\; \mathcal{L}(\mathcal{F}), \qquad e(\ell) = \{ e(x) : x \in \ell \}.

Since ee is injective, distinct lines of SS have distinct images. So the equality says that ee maps the lines of SS one-to-one onto the seven Fano triples. In particular, SS then has exactly 77 lines.

In short, the statement says: for every system SS of 33-element subsets of a 77-point set in which each pair of distinct points lies in exactly one member, some relabelling of the points turns SS's line set into exactly the line set {{i,i+1,i+3}:i∈Z/7}\{\{i,i+1,i+3\} : i \in \mathbb{Z}/7\}. (The general definition of "Fano" applies to systems on nn points and asks for a bijection from those nn points to [7][7]. Here n=7n = 7 is fixed by the type of SS.)

Human review

  • Endorsed by Shuze Chen · Sep 25, 2026

    Confirmed by the moderator at approval.

  • Endorsed by ShapeZero · Sep 25, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph