Having Lean check a certificate — the outside computation searches, Lean confirms

Can 11 points be placed in the plane so that the endpoints of every specified edge are at distance exactly 1?
(A unit-distance graph: the graph whose vertices are points of the plane, with two points joined by an edge when their distance is exactly 1. Here distance 1 is imposed only on the endpoints of edges; nothing is imposed on pairs that are not edges.)

The answer is that it cannot. For none of a certain 117 edge lists can it be done. How to hand this "cannot be done" to a machine to confirm is the subject of this page.

The difficulty is that there is a continuum of placements. The decide of 03 can be used only when the cases can all be listed, and if the search itself is written in Lean, talk of search efficiency gets mixed into the proof. So we separate them.

The work splits in two.

• The outside computation searches for a certificate. Splitting cases with interval arithmetic, it kills off "this placement is impossible" one case at a time and leaves a record of how each was killed. Speed is everything, so any tool will do — a numerical language, search tricks, guesswork. It may even be wrong.
• Lean checks the certificate. A function that reads the certificate and confirms "this really is killed" is written in Lean, and a theorem is proved that if that function returns true, no realization exists. If the certificate is wrong, the check returns false, so there is no need to trust the outside computation.

The only thing trusted is the soundness proof of the checker. The correctness of the search is not trusted. This division has two advantages: the search can be made as fast as you like, and rewriting the search does not require rewriting the Lean side.

A build that has Lean check certificates is always four stages. ① the shape of the data, ② the checking function, ③ the soundness theorem, ④ running the individual certificates with decide. Written small, with just these four stages and the contents swapped out, it looks like this.

import Mathlib

/-! The smallest form of the four stages of having a certificate checked. -/

/-- ① The shape of the certificate (data). An interval with integer endpoints. -/
structure Box where
  lo : ℤ
  hi : ℤ

/-- ② The checking function. Says "this box does not contain 1" using integer comparisons only. -/
def excludesOne (b : Box) : Bool := decide (b.hi < 1) || decide (1 < b.lo)

/-- ③ The soundness theorem. If the check is `true`, a real number in that box is not 1. -/
theorem excludesOne_sound {b : Box} {x : ℝ}
    (hb : excludesOne b = true) (h1 : (b.lo : ℝ) ≤ x) (h2 : x ≤ (b.hi : ℝ)) : x ≠ 1 := by
  rcases Bool.or_eq_true_iff.1 hb with h | h
  · have : (b.hi : ℤ) < 1 := of_decide_eq_true h
    have : (b.hi : ℝ) < 1 := by exact_mod_cast this
    intro hx; rw [hx] at h2; linarith
  · have : (1 : ℤ) < b.lo := of_decide_eq_true h
    have : (1 : ℝ) < (b.lo : ℝ) := by exact_mod_cast this
    intro hx; rw [hx] at h1; linarith

/-- ④ Run an individual certificate with `decide`. -/
theorem box_ok : excludesOne ⟨2, 5⟩ = true := by decide

/-- Joining the two, Lean draws a conclusion about a box produced by the outside computation. -/
example {x : ℝ} (h1 : (2 : ℝ) ≤ x) (h2 : x ≤ 5) : x ≠ 1 :=
  excludesOne_sound box_ok h1 h2

LeanChecked by hand; it went through. The thing to notice is that the theorem in ③ speaks about real numbers, while the computation in ④ touches only integers. Bridging the real-number claim and the computable data is the job of ③, and once that is done, ④ can be added in the same form as many times as you like.

What follows swaps the contents of these four stages for the real thing.

Eliminate square roots from the formulas

The operation that determines coordinates from the distances to three points (trilateration) produces square roots when written naively. Once square roots enter the formulas, interval arithmetic and comparisons both become much heavier.

So one step is split into two. When vertex v is at distance 1 from both already-placed a, b, put u := v − (a+b)/2 and d := b − a; then u and d are orthogonal, and u is a real multiple of d rotated by 90 degrees. Calling that multiple lam, we have |d|²(4 lam² + 1) = 4.

/-- **`trilat_core`**: if `u ⊥ d` and `d ≠ 0`, then `u` is a real multiple of the direction `(−d_y, d_x)` orthogonal to `d`. -/
lemma trilat_core {ux uy dx dy : ℝ} (hD : dx^2 + dy^2 ≠ 0) (hlin : ux*dx + uy*dy = 0) :
    ∃ lam : ℝ, ux = -(lam*dy) ∧ uy = lam*dx

Upper and lower bounds for lam can be checked with integer multiplication alone, without taking a square root. The certificate offers the 2 integers of the bounds, and Lean verifies by multiplication that they are compatible with |d|²(4 lam² + 1) = 4.

/-- **`lam_box`**: from `|d|²·(4 lam² + 1) = 4` and an interval for `|d|²`, produce two boxes for `lam`.
No square root appears; the check is `ℤ` multiplication only. -/
lemma lam_box {lam D : ℝ} {dl dh ll lu : ℤ}
    (hD1 : (dl:ℝ) ≤ (sc:ℝ) * D) (hD2 : (sc:ℝ) * D ≤ (dh:ℝ)) (hdl : 0 < dl)
    (heq : D * (4*lam^2 + 1) = 4)
    (hll : 0 ≤ ll) (hlu : ll ≤ lu)
    (hU : sc*sc*(4*sc - dl) ≤ 4*dl*lu*lu)
    (hL : ll = 0 ∨ 4*dh*ll*ll ≤ sc*sc*(4*sc - dh)) :
    Sem ⟨ll, lu⟩ lam ∨ Sem ⟨-lu, -ll⟩ lam

The key point is that the conclusion is an "or". lam is on either the positive side or the negative side — this becomes the fork in the branching tree.

Make the interval endpoints integers

The endpoints of the interval arithmetic are neither reals nor rationals but integers. With reals one cannot compute; with rationals the denominators blow up at every multiplication. With integers, the kernel's evaluation finishes with integer addition, subtraction, multiplication and comparison alone.

To handle fractions, fixed point at scale 2^40 is used. The meaning "interval I contains the real x" is defined, and soundness is proved for each operation.

/-- The fixed-point scale `2^40`. Written as a literal to make the kernel's evaluation fast. -/
def sc : ℤ := 1099511627776

/-- A closed interval with endpoints in `ℤ` (scale `sc`). -/
structure Ivl where
  lo : ℤ
  hi : ℤ
deriving DecidableEq

/-- `x` lies in interval `I`: `I.lo ≤ sc·x ≤ I.hi`. -/
def Sem (I : Ivl) (x : ℝ) : Prop := (I.lo : ℝ) ≤ (sc:ℝ) * x ∧ (sc:ℝ) * x ≤ (I.hi : ℝ)

def addI (a b : Ivl) : Ivl := ⟨a.lo + b.lo, a.hi + b.hi⟩

def subI (a b : Ivl) : Ivl := ⟨a.lo - b.hi, a.hi - b.lo⟩

def mulI (a b : Ivl) : Ivl :=
  ⟨(min (min (a.lo*b.lo) (a.lo*b.hi)) (min (a.hi*b.lo) (a.hi*b.hi))) / sc,
   -((-(max (max (a.lo*b.lo) (a.lo*b.hi)) (max (a.hi*b.lo) (a.hi*b.hi)))) / sc)⟩

lemma addI_sound {a b : Ivl} {x y : ℝ} (ha : Sem a x) (hb : Sem b y) : Sem (addI a b) (x + y)

lemma mulI_sound {a b : Ivl} {x y : ℝ} (ha : Sem a x) (hb : Sem b y) : Sem (mulI a b) (x * y)

Addition and subtraction are exact; only multiplication rounds. The / sc in mulI rounds down, and the other one rounds up, so the interval widens outward. That it is outward is the content of soundness (mulI_sound); rounding inward would produce false rejections.

Make the edges a list

The graph is not a SimpleGraph but a List (ℕ × ℕ) — a sequence of pairs of vertex numbers. To run certificates with decide, edge membership has to be in computable form. The definition of a realization is split in two stages.

/-- The edge conditions only (nothing imposed on non-edges; injectivity not imposed). -/
def Edges (E : List (ℕ × ℕ)) (x y : ℕ → ℝ) : Prop :=
  ∀ e ∈ E, (x e.1 - x e.2)^2 + (y e.1 - y e.2)^2 = 1

/-- A planar unit-distance realization of the 11-point graph with edge set `E`:
  edges at distance 1, **no constraint on non-edges**, distinct vertices at distinct points. -/
def Realiz (E : List (ℕ × ℕ)) (p : Fin 11 → ℝ × ℝ) : Prop :=
  (∀ e ∈ E, ((p (emb e.1)).1 - (p (emb e.2)).1)^2
      + ((p (emb e.1)).2 - (p (emb e.2)).2)^2 = 1) ∧ Function.Injective p

Edges is the weaker condition (points may coincide), so a negation of Edges yields a negation of Realiz. If it can be closed on the weaker side, close it there — bringing it down to the stronger side afterwards is one line.

Fix the coordinate system

A placement in the plane moves under rotations and translations, so 1 edge is fixed to (0,0)–(1,0). That this loses no generality has to be proved, and in Lean one writes the rotation formula concretely and confirms the equations.

/-- **Normalization**: if edge `ab` exists, a rotation and a translation bring `a = (0,0)` and `b = (1,0)`. -/
lemma normalize (E : List (ℕ × ℕ)) (a b : ℕ) (hab : (a, b) ∈ E) (x y : ℕ → ℝ)
    (h : Edges E x y) :
    ∃ X Y : ℕ → ℝ, Edges E X Y ∧ X a = 0 ∧ Y a = 0 ∧ X b = 1 ∧ Y b = 0

① The shape of the certificate. A branching tree. Boxes are not carried — the checker computes them itself. What is carried is the shape of the tree, the bounds for lam at each branch (2 integers), and the positions of the bisections.

inductive Tr where
  | kill (u w : ℕ) : Tr
  | split (ll lu : ℤ) (tp tm : Tr) : Tr
  | bisx (v : ℕ) (mid : ℤ) (t1 t2 : Tr) : Tr
  | bisy (v : ℕ) (mid : ℤ) (t1 t2 : Tr) : Tr
  | free (u p : ℕ) (t : Tr) : Tr

The meaning of the five branches. split is one step of trilateration, forking on the sign of lam. kill is "the interval for the length of this edge does not contain 1, so this branch is dead". bisx and bisy bisect the box along that axis (obviously sound). free is the step that places one end of an edge in the [-1,1]² around the other end; it is used when the angle is free.

② The checking function. It returns a Bool.

def chk (E : List (ℕ × ℕ)) : Tr → List (ℕ × ℕ × ℕ) → St → Bool
  | .kill u w, _, σ =>
      match σ u, σ w with
      | some A, some B => isEdge E u w && killOK A B
      | _, _ => false
  | .split ll lu tp tm, pl, σ =>
      match pl with
      | [] => false
      | (v, a, b) :: pl' =>
          match σ a, σ b with
          | some A, some B =>
              isEdge E v a && isEdge E v b && (triStep ll lu A B).1 &&
                chk E tp pl' (upd σ v (triStep ll lu A B).2.1) &&
                chk E tm pl' (upd σ v (triStep ll lu A B).2.2)
          | _, _ => false
  | .bisx v mid t1 t2, pl, σ =>
      match σ v with
      | some A =>
          chk E t1 pl (upd σ v (⟨A.1.lo, mid⟩, A.2)) &&
            chk E t2 pl (upd σ v (⟨mid, A.1.hi⟩, A.2))
      | none => false

(The bisy and free branches have the same form.) This function is not a proof. It is simply a program that computes a Bool, and given a wrong certificate it returns false.

③ The soundness theorem. This is the linchpin of the division of labor.

/-- **Soundness of the checker**: if `chk` returns `true`, no realization satisfying that state exists. -/
theorem chk_sound (E : List (ℕ × ℕ)) (x y : ℕ → ℝ) (hE : Edges E x y) :
    ∀ (t : Tr) (pl : List (ℕ × ℕ × ℕ)) (σ : St), Holds σ x y → chk E t pl σ = true → False

The proof is by induction on the structure of Tr. There are five branches, so five cases are filled in, each using "soundness of the interval arithmetic" and "soundness of one trilateration step". Once this is proved, no re-proof is needed however many certificates are added.

Combined with fixing the coordinate system, it becomes the tool for closing a candidate.

/-- **The tool for closing a candidate**: if the check of certificate `t` with plan `pl` passes, no coordinates satisfy the edge conditions. -/
theorem close_edges (E : List (ℕ × ℕ)) (a b : ℕ) (hab : (a, b) ∈ E) (t : Tr)
    (pl : List (ℕ × ℕ × ℕ)) (hchk : chk E t pl (st0 a b) = true) :
    ∀ x y : ℕ → ℝ, ¬ Edges E x y := by
  intro x y h
  obtain ⟨X, Y, hXY, h1, h2, h3, h4⟩ := normalize E a b hab x y h
  exact chk_sound E X Y hXY t pl (st0 a b) (holds_st0 h1 h2 h3 h4) hchk

Leantrilat_core · lam_box · mulI_sound · chk_sound · normalize · close_edges · close_realiz.

④ From here on it is mechanical. For each candidate, line up the edge list, the trilateration order and the certificate tree, and run decide.

def E0 : List (ℕ × ℕ) := [(0, 1), (0, 2), (0, 3), (1, 2), (1, 6), (1, 10), (2, 7), (2, 10), (3, 8), (3, 9), (4, 5), (4, 6), (4, 7), (4, 8), (5, 6), (5, 7), (5, 9), (6, 8), (6, 10), (7, 9), (8, 10), (9, 10)]

def pl0 : List (ℕ × ℕ × ℕ) := [(6, 4, 5), (7, 4, 5), (8, 4, 6), (9, 5, 7), (10, 6, 8), (1, 6, 10), (2, 1, 10), (0, 1, 2), (3, 0, 8)]

theorem chk0 : chk E0 tr0 pl0 (st0 4 5) = true := by decide +kernel

theorem no_edges_0 : ∀ x y : ℕ → ℝ, ¬ Edges E0 x y :=
  close_edges E0 4 5 (by decide) tr0 pl0 chk0

theorem no_realiz_0 : ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E0 p :=
  close_realiz E0 4 5 (by decide) tr0 pl0 chk0

pl0 is the trilateration order ("vertex 6 from 4 and 5, vertex 7 from 4 and 5, …"), and tr0 is the branching tree. tr0 is a single line of nested .split and .kill, and integers like 952205001410 are the lower and upper bounds for lam (at scale 2^40, so around 0.8660… as a real number). This line was written by the outside computation; Lean only reads it and verifies it.

def tr0 : Tr := .split 952205001410 952205001411 (.split 952205001410 952205001411 (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)))) (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))))) (.split 952205001410 952205001411 (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)))) (.split 952205001409 952205001411 (.split 952205001409 952205001411 (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001415 (.kill 10 9) (.kill 10 9))) (.split 952205001409 952205001411 (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)) (.split 952205001406 952205001414 (.kill 10 9) (.kill 10 9)))))

decide +kernel means "decide by the kernel's evaluation alone". Ordinary decide also uses the tactic-side evaluator along the way, but for a large computation it is faster to let the kernel do it directly, and the trust boundary stays the kernel (unlike native_decide).

When all 117 are lined up, the overall theorem is a single statement.

/-- **Main theorem**: none of the edge sets in `cands` (117 classes) has a planar unit-distance realization. -/
theorem hn11_no_realiz : ∀ E ∈ cands, ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p

/-- The version with the edge conditions only (does not use injectivity; stronger). -/
theorem hn11_no_edges : ∀ E ∈ cands, ∀ x y : ℕ → ℝ, ¬ Edges E x y

/-- There are 117 candidates. -/
theorem cands_card : cands.length = 117 := by decide

Leanhn11_no_realiz · hn11_no_edges · cands_card. The nodes total 34,049, and the CPU time was 11 minutes. computation

'hn11_no_realiz' depends on axioms: [propext, Classical.choice, Quot.sound]
'hn11_no_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'cands_card' does not depend on any axioms
'trilat_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'lam_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'chk_sound' depends on axioms: [propext, Classical.choice, Quot.sound]
'chk0' depends on axioms: [propext, Quot.sound]

Two things to notice. Classical.choice does not appear for chk0 (the check of the certificate itself). It closes by the kernel's evaluation, so the axiom of choice is not needed. cands_card uses no axioms at all — it only counts the length of a list.

And sorryAx and Lean.ofReduceBool appear nowhere. decide +kernel is not native_decide, so no axiom is added. This is the line of "make it fast without widening the trust boundary".

Work of the same pattern — the 2,100 candidates on 16 points, and the 296 candidates on 10 points that an intermediate filter discarded — is in Lean too (hn16_no_realiz · hn10_no_realiz). The checker (chk and its soundness) was not rewritten. It was built so as not to depend on the number of vertices, so only the candidate side had to be added.

Let this be written out clearly once. What Lean guarantees goes as far as "the listed candidates cannot be placed"; it does not guarantee "the candidates are all of them".

There are two statements in Lean.

What follows from these two is only "the 117 concrete edge lists have no realization". "The isomorphism classes of 11-point graphs satisfying the conditions are exactly these 117" lies outside Lean. That is an enumeration computation — building isomorphism classes while pruning branches by the number of edges and a lower bound on the degree, and dropping duplicates by isomorphism testing — and it rests on the correctness of that procedure.

So the upper-bound claim that comes out of this material has to be written in the following form.

The certificates are Lean; completeness is computation.

In fact, on the 16-point side there are three places not filled in — completeness of the enumeration, the combinatorial part of the soundness of the intermediate filter, and the isomorphism test for each case. The geometric side (that there is no realization) is in Lean; the combinatorial side (that the candidates are all of them) remains computation. Saying "proved in Lean" without drawing this line would be claiming something that was not claimed.

It is not that there is no road to filling the hole. Running the enumeration itself inside Lean would close it, but then both "soundness of the enumerator" and "completeness of the enumerator" have to be proved, and the latter is far heavier work than the former. Soundness (what is said is correct) and completeness (everything is said) differ in the weight of formalization.

What hn11_no_realiz says is this.

For each element E of the list cands, there is no map p from Fin 11 to the plane such that "the endpoints of every edge of E are at distance 1" and "p is injective".

Four things it does not say.

• It does not say "the candidates are all of them". As in §08.
• It does not say "pairs that are not edges are not at distance 1". Realiz imposes distance 1 only on edges. As a definition of unit-distance graph this is correct (though a definition in which a non-edge pair must not happen to be at distance 1 is also possible), but which definition it is cannot be known without reading the statement.
• "The rounding of the interval arithmetic is in the correct direction" is not a statement; it is the content of a proof. If mulI rounded inward, mulI_sound could not be proved, and things would stop there. That the soundness proof went through is the guarantee of the direction of rounding.
• It says nothing about how the certificates were found. If the outside computation produces a different tree, the same theorem comes out as long as the check passes.

The second is the easiest thing to misread in this material. A constraint not written in the definition is not imposed. Continued in It compiles — but does it say what you meant?

Sources and reproduction

Next: 08 It compiles — but does it say what you meant? — §08 and §09 of this page, written out as a general procedure. Terms are in 12 Glossary.