數學證明：證明 n²+n 恆為偶數，並以反例否定「n²+n+41 恆為質數」

目標與範圍

(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≤r<b。
• divides_def · prerequisite — 整除：對整數 a、b，a∣b 表示存在整數 k 使 b=ak。
• distributive · prerequisite — 分配律：u(v+w)=uv+uw；配合乘法交換律也有 (v+w)u=vu+wu。
• power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• two_nonzero · prerequisite — 實數中 0<1，故 0<1+1=2，所以 2≠0。
• order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
• 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。

逐步主鏈

\text{prove}\ T

\text{premises of G1}\ +\ \text{valid rules}\ \Rightarrow\ T

n\in\mathbb{Z}\ \text{arbitrary}

n=2q+r,\ q,r\in\mathbb{Z},\ 0\le r<2

0\le r<2,\ r\in\mathbb{Z}

r=0\ \lor\ r=1

r=0:\ n=2q

n^2+n=(2q)^2+2q=4q^2+2q

4q^2+2q

2(2q^2+q),\ \text{so}\ 2\mid n^2+n

r=1:\ n=2q+1

n^2+n=(2q+1)^2+(2q+1)=4q^2+6q+2

4q^2+6q+2

2(2q^2+3q+1),\ \text{so}\ 2\mid n^2+n

r=0\Rightarrow 2\mid n^2+n,\quad r=1\Rightarrow 2\mid n^2+n

2\mid n^2+n

2\mid n^2+n\ \text{for the arbitrary}\ n

\forall n\in\mathbb{Z}:\ 2\mid n^2+n\quad(T)

\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

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)}

n=40:\ 40^2+40+41

1681=41\cdot 41

1681=41\cdot 41

1681\ \text{is not prime}

40\in\mathbb{N},\ 40^2+40+41\ \text{not prime}

\neg C

\text{conclusions of S09, S10, S11, S14}

T\ \text{proved};\ C\ \text{refuted}

局部子步與引理

(2q+1)^2

4q^2+4q+1

(4q^2+4q+1)+(2q+1)

4q^2+6q+2

逐步反向審查

• 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、反控制與修訂記錄）