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:
“The moment a man begins to talk about technique that’s proof that he is fresh out of ideas.”
—Raymond Chandler (1888–1959)
“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)