大学
Fermat42が容疑者にいちど名前をつけます:非ゼロのa・bとa⁴ + b⁴ = c²。
事件簿に「数」「その条件」「等式」の3枚が入っているとします。等式の欄を取り出すのは、必要な紙を選ぶ作業です。取り出すだけで新しい等式を証明するわけではありません。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
フォルダから等式の紙を出すようなものです。もとから入っていた証拠を、次の一歩で使えるようにします。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ、束に入っていた証拠を取り出す。 フォルダから等式の紙を出すようなものです。もとから入っていた証拠を、次の一歩で使えるようにします。
入れ子になった連言から欄を取り出す練習:等式は三番目の成分としてしまわれています。h.1.2.2が束からa ^ 4 + b ^ 4 = c ^ 2を取り出します。下の証明がまさにそう使います。
Mathlib · db584cd · Four.lean
/-- Shorthand for three non-zero integers `a`, `b`, and `c` satisfying `a ^ 4 + b ^ 4 = c ^ 2`.We will show that no integers satisfy this equation. Clearly Fermat's Last theorem for n = 4follows. -/def Fermat42 (a b c : ℤ) : Prop :=a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2namespace Fermat42theorem comm {a b c : ℤ} : Fermat42 a b c ↔ Fermat42 b a c := bydelta Fermat42rw [add_comm]tauto
commの証明は小さな機構の見本です:deltaが両辺の定義を展開し、rw [add_comm]が片辺を組み替え、tautoが論理の帳簿を片付けます。近くの補題mulとne_zeroは抜粋のすぐ下にあります——解をk倍する話と、cがゼロになれない話。事件の実質的な仕事は、帳簿のあとで始まります。
事件簿の等式をいちどに束ねる
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
Fermat42が容疑者にいちど名前をつけます:非ゼロのa・bとa⁴ + b⁴ = c²。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
入れ子になった連言から欄を取り出す練習:等式は三番目の成分としてしまわれています。h.1.2.2が束からa ^ 4 + b ^ 4 = c ^ 2を取り出します。下の証明がまさにそう使います。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →