必ず終わる階段

Leanでの使用例・原文の抜粋

Mathlib · db584cd · Three.lean

749/-- Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then750`a ^ 3 + b ^ 3 ≠ c ^ 3`. -/751public theorem fermatLastTheoremThree : FermatLastTheoremFor 3 := by752  let K := CyclotomicField 3 ℚ753  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K754  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _755  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ756  intro a b c u hc ha hb hcdvd coprime H757  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=758  { a := a759    b := b760    c := c761    u := u762    ha := ha763    hb := hb764    hc := hc765    coprime := coprime766    hcdvd := hcdvd767    H := H }768  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'769  obtain ⟨Smin, hSmin⟩ := S.exists_minimal770  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt771  linarith [hSmin Sfin]

このLeanの読み方

証明をゆっくり読みます:三つのobtainが往復を一つずつ分解し、最小の解がもっと小さい解に変わります。そのあと、最小性の不等式hSmin Sfinを算術に渡します。降下の補題が作った「真に小さい回数」と並べると、linarithはただ一つの結論に落ち着きます:Sfinなど最初から存在しなかった。説明文の上のset_optionは、elaborationのヒューリスティックの調整で、数学の一部ではありません。