また、いちばん小さい容疑者を選ぶ

Leanの定義・原文の抜粋

Mathlib · db584cd · Four.lean

58/-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with59a smaller `c` (in absolute value). -/60def Minimal (a b c : ℤ) : Prop :=61  Fermat42 a b c ∧ ∀ a1 b1 c1 : ℤ, Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c162 63/-- if we have a solution to `a ^ 4 + b ^ 4 = c ^ 2` then there must be a minimal one. -/64theorem exists_minimal {a b c : ℤ} (h : Fermat42 a b c) : ∃ a0 b0 c0, Minimal a0 b0 c0 := by65  classical66  let S : Set ℕ := { n | ∃ s : ℤ × ℤ × ℤ, Fermat42 s.1 s.2.1 s.2.2 ∧ n = Int.natAbs s.2.2 }67  have S_nonempty : S.Nonempty := by68    use Int.natAbs c69    rw [Set.mem_ofPred_eq]70    use ⟨a, ⟨b, c⟩⟩71  let m : ℕ := Nat.find S_nonempty72  have m_mem : m ∈ S := Nat.find_spec S_nonempty73  rcases m_mem with ⟨s0, hs0, hs1⟩74  use s0.1, s0.2.1, s0.2.2, hs075  intro a1 b1 c1 h176  rw [← hs1]77  apply Nat.find_min'78  use ⟨a1, ⟨b1, c1⟩⟩

このLeanの読み方

証明は機械的な整礎法です:集合Sは解が実現する|c|を集め、S_nonemptyが与えられた解を据え、Nat.findが最小の要素を選び、Nat.find_min'がそれをすべての解についての全称の主張へ変えます。途中のrcasesが証人の組sを開きます。ここから降下は、いつでも「最小の目盛り」を語れます。