funlean.
順番 20 / 64

高校

四乗は二乗にたためる

四乗は正方形の正方形です。それで指数4の場合は、一つ下の指数の等式にたためます。

まず、身近な例で

2⁴は2²をもう一度二乗して16。3⁴は81。合わせた97は整数の二乗ではありません。これは一例で、定理では許されるすべての組について調べます。

ちいさな確認：考えてみよう

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

2⁴+3⁴=97が平方でないと計算できたら、すべての組について証明できた？

答えと考え方を読む

いいえ、この組の確認だけ。 16+81=97は計算の練習になります。でも、すべてについての主張には、許されるどの組にも通じる理由が必要です。

3段階で考えよう

  1. 四乗は、また正方形です:a ^ 4 = (a ^ 2) ^ 2。つまりa ^ 4 + b ^ 4 = c ^ 4は、(a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2という、指数を一つ下げた同じ形の等式とまったく同じことです。
  2. 定理fermatLastTheoremFourは、場合をFermatLastTheoremFor 4として直接述べ、すぐに下の形へ書き換え、c ^ 2をnot_fermat_42へ渡します。
  3. だからこの事件の捜査対象は一つの問いに要約します:aとbがどちらもゼロでないまま、a ^ 4 + b ^ 4が正方形c ^ 2になれるか?答えはノー。このあとのページが、それを示す降下法をたどります。

小さな例で確かめる

小さいもので試します:16 + 81 = 97。二つの四乗2⁴と3⁴の和は正方形ではなく、他の非ゼロの組でも決して成功しません。

Leanの定義・原文の抜粋

Mathlib · db584cd · Four.lean

theorem fermatLastTheoremFour : FermatLastTheoremFor 4 := by  rw [fermatLastTheoremFor_iff_int]  intro a b c ha hb _ heq  apply @not_fermat_42 _ _ (c ^ 2) ha hb  rw [heq]; ring

このLeanの読み方

rw [fermatLastTheoremFor_iff_int]は自然数の主張を整数へ翻訳し、非ゼロの証拠も引き連れます。書き換え後の目標はa ^ 4 + b ^ 4 ≠ (c ^ 2) ^ 2——まさにnot_fermat_42が禁じる形で、ringが小さな代数の差を閉じます。この五行が場合全体を運びます:ファイルのほかの部分は、すべてnot_fermat_42の支えです。

元の原文 ↗ · L267–271保存した原文全体を開く

この言葉を使う章

7. ベテランたちの事件簿
わからない・道に迷った

ミカのたすけ舟

四乗は二乗にたためる

今は、一つだけ

まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。

言葉をほどこう

四乗は正方形の正方形です。それで指数4の場合は、一つ下の指数の等式にたためます。

このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。

小さな手がかり

小さいもので試します:16 + 81 = 97。二つの四乗2⁴と3⁴の和は正方形ではなく、他の非ゼロの組でも決して成功しません。

閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。

最初の小さな物語から読む →