# 數學證明：證明 n²+n 恆為偶數，並以反例否定「n²+n+41 恆為質數」 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-proof/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-proof-01 · production-20261019-adopted-96 ## 目標與範圍 (1) 在整數的指定語境中，由明示的前提與規則證明定理 T：對每個整數 n，2∣(n²+n)；再由 T 以反證法推出沒有整數 n 使 n²+n 為奇數。(2) 檢驗主張 C：「對每個自然數 n，n²+n+41 是質數」；說明 n=0 到 39 的 40 個正例為何不構成證明，並以 n=40 的反例否定 C。依 MKO：證明須在指定語境中，由已接受的前提、定義與先前結果，經合法推理得到待證命題。語境是 ℤ 的環運算與順序、整除與帶餘除法，以及古典邏輯（G1）。示範直接證明、分情況、全稱推廣、反證法，以及單一反例否定全稱命題。不形式化，不執行 Lean；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - division_algorithm - divides_def - distributive - power_laws - case_analysis - forall_intro - numeric_evaluation - G1 — 語境與可用前提：整數 ℤ 與 ℕ={n∈ℤ ∣ n≥0}，使用規則表中的環運算、順序、整除定義與帶餘除法（含唯一性）；推理規則為古典邏輯的分情況、全稱推廣、反證法與量詞否定。 - G2 — 待證定理 T：對每個整數 n，2∣(n²+n)。 - G3 — 被檢驗的主張 C：對每個 n∈ℕ，n²+n+41 是質數；質數指整數 p≥2，且 p 的正因數只有 1 與 p。 - T — 待證定理：∀n∈ℤ, 2∣(n²+n) - C — 被檢驗的主張：∀n∈ℕ, n²+n+41 是質數 - q,\ r — n 除以 2 的商與餘數 - d\mid m — 存在整數 k 使 m=dk - \mathbb{N} — 非負整數 {n∈ℤ ∣ n≥0} ## 規則與來源 - division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤rv 之一；u0 推出 uwvw。 - eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - add_assoc · prerequisite — 加法結合律：(u+v)+w=u+(v+w)。 - add_comm · prerequisite — 加法交換律：u+v=v+u。 - mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_proof · cited — 給定待證命題 P，證明必須在指定語境中由已接受的前提、定義、公理或先前結果，經合法推理得到 P。 · mko-proof - prime_def · prerequisite — 質數：整數 p 是質數 ⇔ p≥2 且 p 的正因數只有 1 與 p。 - int_no_gap · prerequisite — 整數沒有空隙：對整數 k 與 m，必有 k≤m 或 k≥m+1。 - L_odd_case · lemma — 對每個整數 q：(2q+1)²+(2q+1)=4q²+6q+2。 ## 逐步主鏈 S01 · definition操作前 \text{prove}\ T 操作後 \text{premises of G1}\ +\ \text{valid rules}\ \Rightarrow\ T 條件：無規則：mko_proof · 依賴：G1, G2 葉節點依據：mko_proof + def_intro 依 MKO，證明要在指定語境中，由已接受的前提、定義或先前結果，經合法推理得到待證命題。所以先寫清楚：待證命題是 T（G2）；可用前提是 G1 所列的整數運算、順序、整除定義與帶餘除法；可用的推理是古典邏輯規則。之後每一步都要能指出所用的前提與規則。 S02 · theorem_application操作前 n\in\mathbb{Z}\ \text{arbitrary} 操作後 n=2q+r,\ q,r\in\mathbb{Z},\ 0\le r<2 條件：2>0 規則：division_algorithm · 依賴：G1 葉節點依據：division_algorithm 任取一個整數 n，不對它加任何額外假設（為了最後的全稱推廣）。依帶餘除法（a=n、b=2，2 是正整數），存在整數 q、r 使 n=2q+r 且 0≤r<2。這對負整數也成立，例如 −3=2·(−2)+1。 S03 · case_split操作前 0\le r<2,\ r\in\mathbb{Z} 操作後 r=0\ \lor\ r=1 條件：無規則：int_no_gap · 依賴：S02 葉節點依據：int_no_gap + order_basics + case_analysis r 是整數且 0≤r<2。依 int_no_gap（m=0），r≤0 或 r≥1。若 r≤0，配合 0≤r 得 r=0；若 r≥1，再依 int_no_gap（m=1），r≤1 或 r≥2，而 r<2 排除後者，所以 r=1。因此 r=0 或 r=1，兩個情形涵蓋所有可能。 S04 · equivalent操作前 r=0:\ n=2q 操作後 n^2+n=(2q)^2+2q=4q^2+2q 條件：無規則：power_laws · 依賴：S03 葉節點依據：power_laws + eq_replace + numeric_evaluation 情形 r=0：n=2q。代入得 n²+n=(2q)²+2q；依指數律 (2q)²=2²q²=4q²，所以 n²+n=4q²+2q。 S05 · implies操作前 4q^2+2q 操作後 2(2q^2+q),\ \text{so}\ 2\mid n^2+n 條件：無規則：divides_def · 依賴：S04 葉節點依據：distributive + divides_def + exists_intro 依分配律 4q²+2q=2(2q²+q)；2q²+q 是整數（整數對加法與乘法封閉），所以依整除定義 2∣(n²+n)。 S06 · equivalent操作前 r=1:\ n=2q+1 操作後 n^2+n=(2q+1)^2+(2q+1)=4q^2+6q+2 條件：無規則：L_odd_case · 依賴：S03 葉節點依據：distributive + power_laws + add_assoc + add_comm + numeric_evaluation 情形 r=1：n=2q+1。代入並依引理 L_odd_case 展開，得 n²+n=4q²+6q+2。 S07 · implies操作前 4q^2+6q+2 操作後 2(2q^2+3q+1),\ \text{so}\ 2\mid n^2+n 條件：無規則：divides_def · 依賴：S06 葉節點依據：distributive + divides_def + exists_intro 依分配律 4q²+6q+2=2(2q²+3q+1)；2q²+3q+1 是整數，所以依整除定義 2∣(n²+n)。 S08 · implies操作前 r=0\Rightarrow 2\mid n^2+n,\quad r=1\Rightarrow 2\mid n^2+n 操作後 2\mid n^2+n 條件：無規則：case_analysis · 依賴：S03, S05, S07 葉節點依據：case_analysis S03 的兩個情形涵蓋全部可能，兩個情形都推出 2∣(n²+n)，依分情況論證，對這個任取的 n 有 2∣(n²+n)。 S09 · implies操作前 2\mid n^2+n\ \text{for the arbitrary}\ n 操作後 \forall n\in\mathbb{Z}:\ 2\mid n^2+n\quad(T) 條件：無規則：forall_intro · 依賴：S02, S08 葉節點依據：forall_intro S02 中的 n 是任取的，S02 到 S08 沒有對 n 加任何額外假設，所以依全稱推廣，對每個整數 n 都有 2∣(n²+n)，定理 T 得證。 S10 · implies操作前 \text{suppose}\ n^2+n=2m+1\ \text{for some}\ n,m\in\mathbb{Z} 操作後 \neg\exists n,m\in\mathbb{Z}:\ n^2+n=2m+1 條件：無規則：contradiction · 依賴：S09, division_algorithm 葉節點依據：contradiction + division_algorithm + divides_def 反證法：假設有整數 n、m 使 n²+n=2m+1。由 T（S09）又有整數 k 使 n²+n=2k=2k+0。於是同一個整數 n²+n 除以 2 有兩種帶餘表示，餘數分別是 1 與 0，都滿足 0≤r<2，與帶餘除法的唯一性矛盾。所以沒有整數 n 使 n²+n 為奇數。這是 MKO 所說的反證法：加入結論的否定並導出矛盾。 S11 · implies操作前 C:\ \forall n\in\mathbb{N},\ n^2+n+41\ \text{is prime} 操作後 n^2+n+41\ \text{is prime for}\ 0\le n\le 39\ \text{(finite check only)} 條件：無規則：numeric_evaluation · 依賴：G3 葉節點依據：numeric_evaluation + prime_def 對 n=0 到 39 逐一計算 n²+n+41 並檢查是否為質數（N5，在 40 個整數點上的有限核對），全部是質數。但 C 是對所有自然數的全稱命題，ℕ 是無窮的；這 40 個正例既沒有證明論域有限，也沒有窮盡論域，因此不能建立 C。MKO 第一段正是這樣說的。 S12 · equivalent操作前 n=40:\ 40^2+40+41 操作後 1681=41\cdot 41 條件：無規則：numeric_evaluation · 依賴：G3 葉節點依據：numeric_evaluation + distributive 取 n=40∈ℕ：40²+40+41=1600+40+41=1681；另一方面 41·41=1681。也看得出結構：40²+40+41=40·(40+1)+41=40·41+41=41·41。 S13 · implies操作前 1681=41\cdot 41 操作後 1681\ \text{is not prime} 條件：無規則：prime_def · 依賴：S12 葉節點依據：prime_def + divides_def + numeric_evaluation 41 是 1681 的正因數（1681=41·41），而 41≠1 且 41≠1681。依質數定義，1681 的正因數不只 1 與自身，所以 1681 不是質數。 S14 · implies操作前 40\in\mathbb{N},\ 40^2+40+41\ \text{not prime} 操作後 \neg C 條件：無規則：quantifier_negation · 依賴：S12, S13, G3 葉節點依據：quantifier_negation + exists_intro n=40∈ℕ（40≥0）使 n²+n+41 不是質數，所以 ∃n∈ℕ 使 n²+n+41 不是質數，依量詞否定 C 為假。一個有效反例就足以否定全稱命題，不論之前有多少正例。 S15 · implies操作前 \text{conclusions of S09, S10, S11, S14} 操作後 T\ \text{proved};\ C\ \text{refuted} 條件：無規則：and_intro_elim · 依賴：S09, S10, S11, S14 葉節點依據：and_intro_elim T 由明示前提經合法推理證得，對所有整數成立（S09），並推出 n²+n 永不為奇數（S10）。C 雖有 40 個正例（S11），卻被 n=40 的單一反例否定（S14）。前者是證明；後者說明抽樣不是證明。 ## 局部子步與引理 S06.1 · equivalent操作前 (2q+1)^2 操作後 4q^2+4q+1 條件：無規則：distributive · 依賴：distributive, power_laws 葉節點依據：distributive + power_laws + mul_comm + add_assoc + numeric_evaluation (2q+1)²=(2q+1)(2q+1)=2q·2q+2q·1+1·2q+1·1=4q²+2q+2q+1=4q²+4q+1（分配律兩次、乘法交換律、合併同類項）。 S06.2 · equivalent操作前 (4q^2+4q+1)+(2q+1) 操作後 4q^2+6q+2 條件：無規則：add_assoc · 依賴：S06.1 葉節點依據：add_assoc + add_comm + distributive + numeric_evaluation 依加法結合律與交換律重排：4q²+(4q+2q)+(1+1)；依分配律 4q+2q=(4+2)q=6q，且 1+1=2，得 4q²+6q+2。S06.1 與 S06.2 合起來證得引理 L_odd_case。 ## 逐步反向審查 - S15 · sufficient_goal_reduction · S09, S10, S14, and_intro_elim — 目標 G：證明 T 並判定 C。足夠條件 H：S09、S10 與 S14；H⇒G 只是並列。H 由 G1 到 G3 正向證成，沒有把 G 當作前提；S11 只是對照，不在 H 中。 - S14 · premise_audit · S13, exists_intro, quantifier_negation — 需要反例確實在論域 ℕ 中，且確實不滿足性質（S13）。 - S13 · premise_audit · prime_def, divides_def — 只需一個非平凡的正因數。 - S12 · inverse_equivalence · numeric_evaluation, distributive — 兩邊是同一個整數，可重算（N6、N7、N10）。 - S11 · premise_audit · numeric_evaluation, prime_def — 此步只記錄 40 個有限的計算結果；它不推出 C，後面也沒有把它當作 C 的證明。 - S10 · premise_audit · S09, division_algorithm, contradiction — 矛盾來自餘數唯一；暫時假設中的 n、m 是新名字，結論中沒有它們的自由出現。 - S09 · sufficient_goal_reduction · S02, S08, forall_intro — 目標 G：T。足夠條件 H：對一個沒有額外假設的任意整數 n 證得 2∣(n²+n)；H⇒G 由全稱推廣。H 由 S02 到 S08 從 G1 的前提正向證成，沒有把 T 當作前提。N4 在 n=−20 到 20 的有限核對只是交叉核對，不是證明的一部分。 - S08 · premise_audit · S03, S05, S07, case_analysis — 若只處理 r=0，就只證明了偶數 n 的情形；兩支都必須做。 - S07 · premise_audit · distributive, divides_def, exists_intro — 需要整數見證 2q²+3q+1；N2 獨立核對整個恆等式。 - S06.2 · inverse_equivalence · add_assoc, add_comm, distributive — 只用恆等式重排，雙向成立。 - S06.1 · inverse_equivalence · distributive, mul_comm, add_assoc — 恆等式，倒著讀同樣成立；N3 是獨立核對。 - S06 · inverse_equivalence · L_odd_case — 等值代換，雙向成立；引理在子步中證明。 - S05 · premise_audit · distributive, divides_def, exists_intro — 需要一個整數見證 k=2q²+q；N1 是對所用恆等式的獨立多項式核對。 - S04 · inverse_equivalence · power_laws, eq_replace — 只是等值代換，兩邊是同一個整數。 - S03 · premise_audit · S02, int_no_gap, order_basics — 兩支涵蓋全部可能，由 r 的範圍與整數沒有空隙保證，不是靠看例子。 - S02 · premise_audit · division_algorithm, two_nonzero — 帶餘除法只要求除數是正整數；n 可以是任何整數。 - S01 · premise_audit · G1, G2, mko_proof — 此步只確定證明的語境，不推出新事實。 ## 錯誤控制與反例數值抽樣不是證明MKO 指出常見誤解是把數值抽樣當成一般證明。C 在 n=0 到 39 都成立，卻在 n=40 失敗（S11 到 S14）。同理，N4 在 n=−20 到 20 核對 n²+n 為偶數也只支持那 41 個點；T 對所有整數成立的理由是 S02 到 S09 的推理。分情況必須涵蓋全部可能S03 的兩個情形由帶餘除法與 0≤r<2 保證涵蓋所有整數，包括負整數（例如 −3=2·(−2)+1 落在 r=1）。若只證明 r=0，例如 n=1=2·0+1 就沒有被涵蓋。權威與直覺不是推理規則MKO 也提到把權威引用或未交代規則的直覺當作證明。「某本書說 C 為真」或「看起來 n²+n+41 總是質數」都不是 G1 中的推理規則；n=40 的計算直接否定 C。證明中每一步都要能指出所用的前提與規則（S01）。 - 已計算 n=1 到 100 時 n²+n 都是偶數，所以 T 得證 → reject — 有限個情形不涵蓋 ℤ（無窮，且含負整數）；T 的證明是 S02 到 S09。 - n=0 到 39 時 n²+n+41 都是質數，所以對所有自然數都是質數 → reject — n=40 時得 1681=41·41，不是質數（S12、S13）。 - 只證 r=0 的情形就足以證明 T → reject — n=1=2·0+1 屬於 r=1，沒有被涵蓋（S08）。 - 權威教科書斷言 C，所以 C 為真 → reject — 權威不是推理規則；n=40 是有效反例（S14）。 ## 結論與限制定理 T 成立：對每個整數 n，2∣(n²+n)；證明以帶餘除法把 n 分成 n=2q 與 n=2q+1 兩個情形，分別得 n²+n=2(2q²+q) 與 n²+n=2(2q²+3q+1)，再全稱推廣。由 T 以反證法得：沒有整數 n 使 n²+n 為奇數。主張 C 為假：雖然 n=0 到 39 時 n²+n+41 都是質數，但 n=40 時它等於 1681=41·41。 - N4 是 n 從 −20 到 20 的有限核對，N5 是 n 從 0 到 39 的有限核對；兩者都不證明任何全稱命題，T 的證明在 S02 到 S09。 - 帶餘除法（含唯一性）與整數的環、序性質作為前提使用，不在此由更基本的公理推出。 ## 驗證及來源綁定 10 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 2c088a296a9a9f16755f489459feaca7850399ca52c46b4d09bc6cc6e9d310f7 - original source SHA-256: 2c088a296a9a9f16755f489459feaca7850399ca52c46b4d09bc6cc6e9d310f7 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-proof-01.json)