Mathematical proof: proving n²+n is always even, and refuting 'n²+n+41 is always prime' by a counterexample

Goal and scope

(1) In a stated context for the integers, prove from explicit premises and rules the theorem T: for every integer n, 2∣(n²+n); then derive from T by contradiction that no integer n makes n²+n odd. (2) Test the claim C: 'for every natural number n, n²+n+41 is prime'; explain why the 40 positive cases n=0 to 39 do not constitute a proof, and refute C by the counterexample n=40.

Follows the MKO: a proof must derive the proposition within a stated context from accepted premises, definitions and earlier results by valid inference. The context is the ring operations and order of ℤ, divisibility and the division algorithm, and classical logic (G1). It illustrates direct proof, proof by cases, universal generalization, proof by contradiction, and refuting a universal statement by one counterexample. It is not formalized, Lean is not run, and the canonical MKO and its English edition are not changed.

Givens and symbols

• division_algorithm
• divides_def
• distributive
• power_laws
• case_analysis
• forall_intro
• numeric_evaluation

• G1 — Context and usable premises: the integers ℤ and ℕ={n∈ℤ ∣ n≥0}, with the ring operations, order, definition of divisibility and division algorithm (including uniqueness) from the glossary; inference rules are the classical ones for cases, generalization, contradiction and negating quantifiers.
• G2 — Theorem T to prove: for every integer n, 2∣(n²+n).
• G3 — Claim C under test: for every n∈ℕ, n²+n+41 is prime, where a prime is an integer p≥2 whose only positive divisors are 1 and p.

• T — the theorem to prove: ∀n∈ℤ, 2∣(n²+n)
• C — the claim under test: ∀n∈ℕ, n²+n+41 is prime
• q,\ r — the quotient and remainder of n by 2
• d\mid m — there is an integer k with m=dk
• \mathbb{N} — the nonnegative integers {n∈ℤ ∣ n≥0}

Rules and sources

• division_algorithm · prerequisite — Division algorithm: for an integer a and a positive integer b there are unique integers q, r with a=bq+r and 0≤r<b.
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_proof · cited — Given a proposition P to be proved, a proof must derive P within a specified context from accepted premises, definitions, axioms, or earlier results by valid inference. · mko-proof
• prime_def · prerequisite — Prime: an integer p is prime ⇔ p≥2 and the only positive divisors of p are 1 and p.
• int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1.
• L_odd_case · lemma — For every integer q: (2q+1)²+(2q+1)=4q²+6q+2.

Main derivation

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

Substeps and lemmas

(2q+1)^2

4q^2+4q+1

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

4q^2+6q+2

Reverse audits

• S15 · sufficient_goal_reduction · S09, S10, S14, and_intro_elim — Goal G: prove T and decide C. Sufficient condition H: S09, S10 and S14; H⇒G just lists them. H is proved forwards from G1 to G3 without using G as a premise; S11 is only a contrast and is not part of H.
• S14 · premise_audit · S13, exists_intro, quantifier_negation — The counterexample must lie in the domain ℕ and must really fail the property (S13).
• S13 · premise_audit · prime_def, divides_def — One nontrivial positive divisor is enough.
• S12 · inverse_equivalence · numeric_evaluation, distributive — Both sides are the same integer and can be recomputed (N6, N7, N10).
• S11 · premise_audit · numeric_evaluation, prime_def — This step only records 40 finite computations; it does not imply C, and no later step uses it as a proof of C.
• S10 · premise_audit · S09, division_algorithm, contradiction — The contradiction comes from uniqueness of the remainder; the n, m of the temporary assumption are fresh names with no free occurrence in the final conclusion.
• S09 · sufficient_goal_reduction · S02, S08, forall_intro — Goal G: T. Sufficient condition H: 2∣(n²+n) proved for an arbitrary integer n with no extra assumption; H⇒G by generalization. H is proved forwards from the premises of G1 in S02 to S08, never using T as a premise. The finite check N4 for n=−20 to 20 is only a cross-check, not part of the proof.
• S08 · premise_audit · S03, S05, S07, case_analysis — Treating only r=0 would prove the claim only for even n; both branches are required.
• S07 · premise_audit · distributive, divides_def, exists_intro — The integer witness 2q²+3q+1 is needed; N2 checks the whole identity independently.
• S06.2 · inverse_equivalence · add_assoc, add_comm, distributive — Only identities are used to rearrange, so the step is two-way.
• S06.1 · inverse_equivalence · distributive, mul_comm, add_assoc — An identity, valid read backwards; N3 is an independent check.
• S06 · inverse_equivalence · L_odd_case — A replacement of equals, two-way; the lemma is proved in the sub-steps.
• S05 · premise_audit · distributive, divides_def, exists_intro — An integer witness k=2q²+q is needed; N1 is an independent polynomial check of the identity used.
• S04 · inverse_equivalence · power_laws, eq_replace — Only a replacement of equals; both sides are the same integer.
• S03 · premise_audit · S02, int_no_gap, order_basics — That the two branches cover everything follows from the range of r and the absence of gaps in the integers, not from looking at examples.
• S02 · premise_audit · division_algorithm, two_nonzero — The division algorithm only requires a positive divisor; n may be any integer.
• S01 · premise_audit · G1, G2, mko_proof — This step only fixes the context of the proof and derives no new fact.

Error controls and negative controls

Numerical sampling is not proof

The MKO names the mistake of taking numerical sampling as a general proof. C holds for n=0 to 39 yet fails at n=40 (S11 to S14). Likewise N4, which checks that n²+n is even for n=−20 to 20, supports only those 41 points; the reason T holds for every integer is the reasoning of S02 to S09.

Cases must cover every possibility

The two cases of S03 are guaranteed by the division algorithm and 0≤r<2 to cover every integer, negatives included (for example −3=2·(−2)+1 falls under r=1). Proving only r=0 would leave, for example, n=1=2·0+1 uncovered.

Authority and intuition are not inference rules

The MKO also mentions treating appeals to authority or unexplained intuition as proof. 'A book says C is true' or 'n²+n+41 looks always prime' are not inference rules of G1; the computation at n=40 refutes C outright. Every step of a proof must name the premises and rules it uses (S01).

• n²+n was computed to be even for n=1 to 100, so T is proved → reject — Finitely many cases do not cover ℤ (infinite, with negatives); the proof of T is S02 to S09.
• n²+n+41 is prime for n=0 to 39, so it is prime for every natural number → reject — At n=40 it is 1681=41·41, not prime (S12, S13).
• Proving the case r=0 alone proves T → reject — n=1=2·0+1 has r=1 and is not covered (S08).
• An authoritative textbook asserts C, so C is true → reject — Authority is not an inference rule; n=40 is a valid counterexample (S14).

Result and limitations

Theorem T holds: for every integer n, 2∣(n²+n); the proof splits n by the division algorithm into n=2q and n=2q+1, obtaining n²+n=2(2q²+q) and n²+n=2(2q²+3q+1), and then generalizes. From T, by contradiction, no integer n makes n²+n odd. Claim C is false: although n²+n+41 is prime for n=0 to 39, at n=40 it equals 1681=41·41.

• N4 is a finite check for n from −20 to 20 and N5 a finite check for n from 0 to 39; neither proves any universal statement, and the proof of T is S02 to S09.
• The division algorithm (with uniqueness) and the ring and order properties of the integers are used as premises and are not derived here from more basic axioms.

Verification and source binding

10 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 2c088a296a9a9f16755f489459feaca7850399ca52c46b4d09bc6cc6e9d310f7
• original source SHA-256: 2c088a296a9a9f16755f489459feaca7850399ca52c46b4d09bc6cc6e9d310f7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)