Example Proof
Isabelle's proof language Isar aims to support proofs that are both human-readable and machine-checkable. For example, the proof that the square root of two is not rational can be written as follows.
theorem sqrt2_not_rational: "sqrt (real 2) ∉ ℚ" proof assume "sqrt (real 2) ∈ ℚ" then obtain m n :: nat where n_nonzero: "n ≠ 0" and sqrt_rat: "¦sqrt (real 2)¦ = real m / real n" and lowest_terms: "gcd m n = 1" .. from n_nonzero and sqrt_rat have "real m = ¦sqrt (real 2)¦ * real n" by simp then have "real (m²) = (sqrt (real 2))² * real (n²)" by (auto simp add: power2_eq_square) also have "(sqrt (real 2))² = real 2" by simp also have "... * real (m²) = real (2 * n²)" by simp finally have eq: "m² = 2 * n²" .. hence "2 dvd m²" .. with two_is_prime have dvd_m: "2 dvd m" by (rule prime_dvd_power_two) then obtain k where "m = 2 * k" .. with eq have "2 * n² = 2² * k²" by (auto simp add: power2_eq_square mult_ac) hence "n² = 2 * k²" by simp hence "2 dvd n²" .. with two_is_prime have "2 dvd n" by (rule prime_dvd_power_two) with dvd_m have "2 dvd gcd m n" by (rule gcd_greatest) with lowest_terms have "2 dvd 1" by simp thus False by arith qedRead more about this topic: Isabelle (proof Assistant)
Famous quotes containing the word proof:
“a meek humble Man of modest sense,
Who preaching peace does practice continence;
Whose pious life’s a proof he does believe,
Mysterious truths, which no Man can conceive.”
—John Wilmot, 2d Earl Of Rochester (1647–1680)
“There is no better proof of a man’s being truly good than his desiring to be constantly under the observation of good men.”
—François, Duc De La Rochefoucauld (1613–1680)