$S$ is the Fano plane up to relabelling

Definition

FanoUnique_isFano

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

combinatoricsfano-planesteiner-triple-systems

Let $S$ be a Steiner triple system on the points $\{0, \dots, n-1\}$ . $S$ is the Fano plane up to relabelling if there is a bijection $e$ from its points to $\{0, \dots, 6\}$ that carries its lines exactly onto the lines of the Fano plane:

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

where $e(\ell) = \{e(x) : x \in \ell\}$ . This forces $n = 7$ and exactly seven lines.

Formalization Note IsFano S is ∃ e : Fin n ≃ Fin 7, S.lines.image (fun l => l.map e.toEmbedding) = fano.lines. STS and fano are the published definitions of the companion mission The role postulates force exactly seven points, imported unchanged.

Definition code

import Mathlib
import Definitions.Def_RolesForceSeven_fano

namespace FanoUnique

open RolesForceSeven

/-- S is the Fano plane up to relabelling: a bijection of points carries S's
lines exactly onto the Fano plane's lines. -/
def IsFano {n : ℕ} (S : STS n) : Prop :=
  ∃ e : Fin n ≃ Fin 7,
    S.lines.image (fun l => l.map e.toEmbedding) = fano.lines

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))"); Fano lines as in the Prove2Me definition RolesForceSeven.fano: 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

Definition IsFano. For a natural number $n$ (an implicit parameter) and a structure $S$ of type "STS on $n$ points", IsFano $S$ is the proposition defined below. The points are $[n] = \{0, 1, \dots, n-1\}$ .

What an "STS on $n$ points" is (imported definition). It is a finite family $\mathcal{L}(S)$ of subsets of $[n]$ , called lines, together with proofs of two conditions:

every line $\ell \in \mathcal{L}(S)$ has exactly $3$ elements;
for any two points $x \ne y$ in $[n]$ there is exactly one line $\ell \in \mathcal{L}(S)$ with $x \in \ell$ and $y \in \ell$ .

Nothing else is required. In particular $n$ is arbitrary (no congruence condition is stated), points are not required to lie on a line, and for $n \le 1$ the second condition is vacuous, so for $n \in \{0,1\}$ the empty family of lines is allowed. Only the family $\mathcal{L}(S)$ enters the definition of IsFano; the two conditions are proofs attached to $S$ .

The reference system $\mathcal{F}$ (imported definition fano). The points are $\mathbb{Z}/7 = \{0,\dots,6\}$ with addition modulo $7$ . For $i \in \mathbb{Z}/7$ put

L_i = \{\, i,\ i+1,\ i+3 \,\} \pmod 7,

and let the lines of $\mathcal{F}$ be $\{L_i : i \in \mathbb{Z}/7\}$ . Explicitly these are the seven sets

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

which are pairwise distinct. The file checks by exhaustive computation that each has $3$ elements and that every pair of distinct points of $\mathbb{Z}/7$ lies in exactly one of them, so $\mathcal{F}$ is an STS on $7$ points.

The definition. IsFano $S$ holds if and only if

\exists\, e : [n] \to \{0,\dots,6\} \text{ a bijection such that } \{\, e(\ell) : \ell \in \mathcal{L}(S) \,\} = \{\, L_i : i \in \mathbb{Z}/7 \,\},

where $e(\ell) = \{ e(x) : x \in \ell \}$ is the image of the line $\ell$ , and the equality is equality of families of subsets of $\{0,\dots,6\}$ (every image of a line of $S$ is one of the $L_i$ , and every $L_i$ is the image of some line of $S$ ). Since $e$ is injective, distinct lines of $S$ have distinct images, so this says $e$ induces a bijection from the lines of $S$ onto the seven lines of $\mathcal{F}$ ; in particular $S$ then has exactly $7$ lines.

Degenerate cases. A bijection $[n] \to \{0,\dots,6\}$ exists only when $n = 7$ ; hence for every $n \ne 7$ and every STS $S$ on $n$ points, IsFano $S$ is false. For $n = 7$ it asserts that some relabelling (permutation) of the seven points carries the line family of $S$ exactly onto the line family $\{L_i\}$ above. The bijection $e$ is only asserted to exist; it is not unique or specified.

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

SSS is the Fano plane up to relabelling

$S$ is the Fano plane up to relabelling