The Fano plane as a Steiner triple system on $7$ points

Definition

RolesForceSeven_fano

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

combinatoricsfano-planesteiner-triple-systems

For $i \in \mathbb{Z}/7\mathbb{Z}$ let $L_i = \{i,\ i+1,\ i+3\}$ , with addition modulo $7$ . The Fano plane is the Steiner triple system on $\{0, \dots, 6\}$ whose lines 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\}.

Every line has three points, and every two distinct points lie on exactly one line.

Formalization Note fanoLine i is $L_i$ in Finset (Fin 7), and fano : STS 7 has lines Finset.univ.image fanoLine. The two structure properties are checked by finite computation (decide).

Definition code

import Mathlib
import Definitions.Def_RolesForceSeven_sts

namespace RolesForceSeven

/-- The Fano plane: lines {i, i+1, i+3} mod 7. -/
def fanoLine (i : Fin 7) : Finset (Fin 7) := {i, i + 1, i + 3}

set_option maxRecDepth 100000 in
def fano : STS 7 where
  lines := Finset.univ.image fanoLine
  card_three := by decide
  pair_unique := by
    have hex : ∀ x y : Fin 7, x ≠ y → ∃ i, x ∈ fanoLine i ∧ y ∈ fanoLine i := by decide
    have huniq : ∀ x y : Fin 7, x ≠ y → ∀ i j, x ∈ fanoLine i → y ∈ fanoLine i →
        x ∈ fanoLine j → y ∈ fanoLine j → fanoLine i = fanoLine j := by decide
    intro x y hxy
    obtain ⟨i, hxi, hyi⟩ := hex x y hxy
    refine ⟨fanoLine i, ⟨Finset.mem_image_of_mem _ (Finset.mem_univ i), hxi, hyi⟩, ?_⟩
    rintro l ⟨hl, hxl, hyl⟩
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.1 hl
    exact huniq x y hxy j i hxl hyl hxi hyi

end RolesForceSeven

Source

Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3, Theorem 3.3 and Theorem 3.6 (the Fano plane): https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf ; corrected in "Errata — C1 Formal Proofs (Sections 3 and 6)", Section 3: https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md ; public references: Wikipedia, "Steiner system" (Steiner triple systems, replication number): https://en.wikipedia.org/wiki/Steiner_system ; Wikipedia, "Fano plane": https://en.wikipedia.org/wiki/Fano_plane ; Wikipedia, "Octonion" (Fano plane mnemonic for the multiplication of imaginary units): https://en.wikipedia.org/wiki/Octonion

Read-back

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

Background: the structure being built. In the imported file, a Steiner-triple-system object on $n$ points ( $n \in \mathbb{N}$ ) has point set $\{0,1,\dots,n-1\}$ and is a bundle of three things:

a finite set $\mathcal{L}$ of subsets of the points (the "lines");
a proof that every $l \in \mathcal{L}$ has exactly $3$ elements;
a proof that for every two points $x \neq y$ there is exactly one set $l$ with $l \in \mathcal{L}$ , $x \in l$ and $y \in l$ .

Nothing else is required: the object does not record or require a particular number of lines. (The imported file also defines a "role colouring" predicate, but the file under review does not use it.)

fanoLine. For each $i$ in the points $\{0,1,\dots,6\}$ of $\mathbb{Z}/7\mathbb{Z}$ , the set $L_i$ is

L_i = \{\, i,\ i+1,\ i+3 \,\} \subseteq \{0,1,\dots,6\},

where addition is modulo $7$ (it wraps around, e.g. $5+3 = 1$ ). Written out, the seven sets are

\begin{aligned} L_0 &= \{0,1,3\}, & L_1 &= \{1,2,4\}, & L_2 &= \{2,3,5\}, & L_3 &= \{3,4,6\},\\ L_4 &= \{0,4,5\}, & L_5 &= \{1,5,6\}, & L_6 &= \{0,2,6\}. \end{aligned}

These are the translates modulo $7$ of the difference set $\{0,1,3\}$ . They are pairwise distinct and each has three distinct elements.

fano. This is a Steiner-triple-system object on $n = 7$ points whose line set is the image of the map $i \mapsto L_i$ over all $i \in \{0,\dots,6\}$ :

\mathcal{L} = \{\, L_i : i \in \mathbb{Z}/7\mathbb{Z} \,\} = \{L_0, L_1, \dots, L_6\}.

Because the seven $L_i$ are pairwise distinct, $\mathcal{L}$ has $7$ members. This count is not stated or proved in the file, but it follows from the explicit list above. The file proves the two required properties:

Every line has 3 points. For each $l \in \mathcal{L}$ , $|l| = 3$ . This is checked by exhaustive computation.
Every pair of distinct points lies on exactly one line. The file first uses exhaustive computation to check two facts over all points:
- (a) for all $x \neq y$ in $\mathbb{Z}/7\mathbb{Z}$ there is an $i$ with $x, y \in L_i$ ;
- (b) for all $x \neq y$ and all $i, j$ , if $x, y \in L_i$ and $x, y \in L_j$ , then $L_i = L_j$ .
From (a) and (b) it concludes that for all $x \neq y$ there is a unique $l$ with $l \in \mathcal{L}$ , $x \in l$ and $y \in l$ . Existence comes from (a) with $l = L_i$ . For uniqueness, any such $l$ equals some $L_j$ , because it belongs to $\mathcal{L}$ , and then (b) gives $L_j = L_i$ .

The object is therefore a concrete, fully specified line system on $\{0,\dots,6\}$ with exactly the seven lines $L_0, \dots, L_6$ listed above. It carries no further data or properties.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ShapeZero · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Fano plane as a Steiner triple system on 777 points

The Fano plane as a Steiner triple system on $7$ points