もっと小さい容疑者が現れる

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

Mathlib · db584cd · Four.lean

239  -- from m = r ^ 2 + s ^ 2 we now get a new solution to a ^ 4 + b ^ 4 = c ^ 2:240  have hh : i ^ 2 = j ^ 4 + k ^ 4 := by grind241  have hn : n ≠ 0 := by grind242  -- and it has a smaller c: from c = m ^ 2 + n ^ 2 we see that m is smaller than c, and i ^ 2 = m.243  have hic : Int.natAbs i < Int.natAbs c := by244    apply Int.ofNat_lt.mp245    rw [← Int.eq_natAbs_of_nonneg (le_of_lt hc)]246    apply lt_of_le_of_lt (Int.natAbs_le_self_sq i)247    rw [← hi, ht3]248    apply lt_of_le_of_lt (Int.le_self_sq m)249    exact lt_add_of_pos_right (m ^ 2) (sq_pos_of_ne_zero hn)250  have hic' : Int.natAbs c ≤ Int.natAbs i := by251    apply h.2 j k i252    exact ⟨hj0, hk0, hh.symm⟩253  apply absurd (not_le_of_gt hic) (not_not.mpr hic')

このLeanの読み方

最後の行が要点です:hhが新しい解の等式をj ^ 4とk ^ 4から組み上げ、hicが|i| ≤ i ^ 2 = m < m ^ 2 < m ^ 2 + n ^ 2 = cとつなぎ、hic'が最小性の仮定h.2を三つ組(j, k, i)に適用します。absurdが主張と否定を並べます——華麗さではなく、算術の正直さ。これは17世紀にフェルマーが歩いた階段で、いまも荷を運びます。