Formal proofs in geometry
Topic
Traditional mathematical proofs are written in a way to make them
easily understood by mathematicians. Routine logical steps are omitted.
An enormous amount of context is assumed on the part of the reader.
Proofs, especially in topology and geometry, rely on intuitive
arguments in situations where a trained mathematician would be capable
of translating those intuitive arguments into a more rigorous argument.
In a formal proof, all the intermediate logical steps are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors. It is generally considered a major undertaking to transcribe a traditional proof into a formal proof.
In recent years, a number of fundamental theorems in mathematics have been formally verified, including the Prime Number Theorem, the Four Color Theorem, and the Jordan Curve Theorem.
In a formal proof, all the intermediate logical steps are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors. It is generally considered a major undertaking to transcribe a traditional proof into a formal proof.
In recent years, a number of fundamental theorems in mathematics have been formally verified, including the Prime Number Theorem, the Four Color Theorem, and the Jordan Curve Theorem.
Speakers
Additional Information
PIMS Distinguished Chair Lectures 2006
Thomas C. Hales (University of Pittsburgh)
