Transcript four color theorem

Lecture 5
1.6 Introduction to Proofs
1.7 Proof Methods and Strategy
Introduction
Proof Terminology
theorem - a statement that can be shown to be true (commonly refers to major results only)
proposition - less important fact or result
lemma - a less important theorem that is used in a step in the proof of a major theorem
proof - method to demonstrate that a theorem or proposition
axiom - also called a postulate is a statement that is assumed to be true
corollary - a theorem that can be established directly from a theorem
conjecture - a statement that is being proposed to be true, but not yet proved
Direct Proof
Proof by Contraposition
Proof by Contradiction
Mistakes in Proofs
Circular Reasoning
Exhaustive Proof
Proof by Cases
Existence Proof
A Constructive Existence Proof
Candidate for a Computer Program
A Nonconstructive Existence Proof
Uniqueness Proof
Counterexamples
Candidate for a Computer Program
Important Open Problems
Other Open Problems
Computer-Assisted Proofs
A computer-assisted proof is a mathematical proof that has been at least partially generated by
computer.
Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of
a mathematical theorem. The idea is to use a computer program to perform lengthy computations,
and to provide a proof that the result of these computations implies the given theorem. In 1976,
the four color theorem was the first major theorem to be verified using a computer program; the
Kepler conjecture followed in 1998.
Attempts have also been made in the area of artificial intelligence research to create smaller,
explicit, new proofs of mathematical theorems from the bottom up using machine reasoning
techniques such as heuristic search. Such automated theorem provers have proved a number
of new results and found new proofs for known theorems. Additionally, interactive proof
assistants allow mathematicians to develop human-readable proofs which are nonetheless
formally verified for correctness. Since these proofs are generally human-surveyable (albeit with
difficulty, as with the proof of the Robbins conjecture) they do not share the controversial
implications of computer-aided proofs-by-exhaustion.
http://en.wikipedia.org/wiki/Computer-assisted_proof
Four Color Theorem
In mathematics, the four color theorem, or the four color map theorem, states that given any
separation of a plane into contiguous regions, called a map, the regions can be colored using at most
four colors so that no two adjacent regions have the same color. Two regions are called adjacent only
if they share a border segment, not just a point.
The four color theorem was proved in 1976 by Kenneth Appel
and Wolfgang Haken. It was the first major theorem to be
proved using a computer. Appel and Haken's approach started
by showing there is a particular set of 1,936 maps, each of
which cannot be part of a smallest-sized counterexample to the
four color theorem. Appel and Haken used a special-purpose
computer program to check each of these maps had this
property.
To dispel remaining doubt about the Appel–Haken proof, a
simpler proof using the same ideas and still relying on
computers was published in 1997 by Robertson, Sanders,
Seymour, and Thomas. Additionally in 2005, the theorem was
proven by Georges Gonthier with general purpose theorem
proving software.
http://en.wikipedia.org/wiki/Four_color_theorem
Kepler Conjecture
The Kepler conjecture, named after Johannes
Kepler, is a mathematical conjecture about sphere
packing in three-dimensional Euclidean space. It
says that no arrangement of equally sized spheres
filling space has a greater average density than that
of the cubic close packing (face-centered cubic) and
hexagonal close packing arrangements. The density
of these arrangements is slightly greater than 74%.
In 1998 Thomas Hales, following an approach suggested
by Fejes Tóth (1953), announced that he had a proof of the
Kepler conjecture. Hales' proof is a proof by exhaustion
involving checking of many individual cases using
complex computer calculations. Referees have said that
they are "99% certain" of the correctness of Hales' proof.
So the Kepler conjecture is now very close to being
accepted as a theorem.
http://en.wikipedia.org/wiki/Kepler_conjecture
Automated Reasoning and Theorem Proving
Automated reasoning is an area of computer science dedicated to understanding different aspects of
reasoning in a way that allows the creation of software which allows computers to reason completely
or nearly completely automatically. As such, it is usually considered a subfield of artificial intelligence,
but it also has strong connections to theoretical computer science and even philosophy.
The most developed subareas of automated reasoning probably are automated theorem proving (and
the less automated but more pragmatic subfield of interactive theorem proving) and automated proof
checking (viewed as guaranteed correct reasoning under fixed assumptions), but extensive work has
also been done in reasoning by analogy induction and abduction.
http://en.wikipedia.org/wiki/Automated_reasoning