Prove2Me

Normal form: the lines through 00 can be made {0,1,2},{0,3,4},{0,5,6}\{0,1,2\}, \{0,3,4\}, \{0,5,6\}

Proved
FanoUnique.normal_form

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

combinatoricsfano-planesteiner-triple-systems

Let SS be a Steiner triple system on {0,…,6}\{0, \dots, 6\}. There is a permutation ee of {0,…,6}\{0, \dots, 6\} such that, after relabelling every point xx as e(x)e(x), the three sets

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

are lines. The three lines through any point split the other six points into three pairs; send the point to 00 and the pairs to {1,2},{3,4},{5,6}\{1,2\}, \{3,4\}, \{5,6\}.

Preamble
import Mathlib
import Definitions.Def_FanoUnique_isFano
Formal statement
namespace FanoUnique

open RolesForceSeven

theorem normal_form (S : STS 7) :
    ∃ e : Fin 7 ≃ Fin 7,
      ({0, 1, 2} : Finset (Fin 7)) ∈ S.lines.image (fun l => l.map e.toEmbedding) ∧
      ({0, 3, 4} : Finset (Fin 7)) ∈ S.lines.image (fun l => l.map e.toEmbedding) ∧
      ({0, 5, 6} : Finset (Fin 7)) ∈ S.lines.image (fun l => l.map e.toEmbedding) := by
  sorry

end FanoUnique
Source
Shape Zero LLC, "Formal Proofs of the C1 Verification Package" (August 2026), §3, proof of Theorem 3.3 ("Uniqueness of STS(7) is classical"); this is a step of the standard textbook proof, supplying the step C1 calls 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 normal_form. Let [7]={0,1,2,3,4,5,6}[7] = \{0,1,2,3,4,5,6\} denote the seven-element point set (the integers mod 7, used here only as labels). The statement is about an arbitrary structure SS of the type called a "Steiner triple system on 7 points". Unfolding the definition, such an SS consists of:

  • a finite set LS\mathcal{L}_S of subsets of [7][7], called lines;
  • the condition that every line has exactly 3 elements: ∣l∣=3|l| = 3 for all l∈LSl \in \mathcal{L}_S;
  • the condition that any two distinct points lie on exactly one common line: for all x,y∈[7]x, y \in [7] with x≠yx \neq y there is a unique ll with l∈LSl \in \mathcal{L}_S, x∈lx \in l and y∈ly \in l.

No other conditions are imposed (for example, nothing about the number of lines is stated; it follows from the two conditions). The only hypothesis of the theorem is that SS is such a structure; there are no other assumptions. The hypothesis is satisfiable: the imported cyclic system with lines {i,i+1,i+3}\{i, i+1, i+3\} (addition mod 7), i∈[7]i \in [7], is one such structure.

The theorem asserts: for every such SS, there exists a bijection (permutation) e:[7]→[7]e : [7] \to [7] such that, writing

e(LS)={ e(l):l∈LS },e(l)={e(p):p∈l},e(\mathcal{L}_S) = \{\, e(l) : l \in \mathcal{L}_S \,\}, \qquad e(l) = \{ e(p) : p \in l \},

for the set of images of the lines under ee, all three of the following hold:

{0,1,2}∈e(LS),{0,3,4}∈e(LS),{0,5,6}∈e(LS).\{0,1,2\} \in e(\mathcal{L}_S), \qquad \{0,3,4\} \in e(\mathcal{L}_S), \qquad \{0,5,6\} \in e(\mathcal{L}_S).

Equivalently, for the same single permutation ee, each of the preimages e−1({0,1,2})e^{-1}(\{0,1,2\}), e−1({0,3,4})e^{-1}(\{0,3,4\}), e−1({0,5,6})e^{-1}(\{0,5,6\}) is a line of SS. These are three 3-element sets that pairwise intersect exactly in the point 00 and together cover all seven points; so the statement says SS can be relabelled so that its three lines through the point labelled 00 are exactly {0,1,2}\{0,1,2\}, {0,3,4}\{0,3,4\}, {0,5,6}\{0,5,6\}. Nothing is asserted about the remaining lines of SS, and ee is not claimed to be unique.

The imported files also define a predicate "SS is isomorphic to the cyclic Fano system above" (existence of a bijection carrying LS\mathcal{L}_S exactly onto the Fano lines) and a notion of "role colouring"; neither appears in this statement.

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