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:
“There are some persons in this world, who, unable to give better proof of being wise, take a strange delight in showing what they think they have sagaciously read in mankind by uncharitable suspicions of them.”
—Herman Melville (1819–1891)
“If we view our children as stupid, naughty, disturbed, or guilty of their misdeeds, they will learn to behold themselves as foolish, faulty, or shameful specimens of humanity. They will regard us as judges from whom they wish to hide, and they will interpret everything we say as further proof of their unworthiness. If we view them as innocent, or at least merely ignorant, they will gain understanding from their experiences, and they will continue to regard us as wise partners.”
—Polly Berrien Berends (20th century)