Great Ideas in Theoretical Computer Science - On Proofs

This lecture introduces the nature of mathematical proof and techniques for finding and writing proofs. It also discusses computer-assisted and computer-formalized proofs, with examples including the Four Color Theorem and the Kepler conjecture.

Syllabus

15-251: Great Theoretical ideas in Computer Science Spring 2016, Lecture 1.5
Proposition
Banach-Tarski Theorem
What is a proof?
Proofs — prehistory
Proofs — 19th century
Principia Mathematica, ca. 1912
Classification of Finite Simple Groups
More anecdotes
Kepler Conjecture
Computer-assisted proof
Computer-formalized proofs
Proof of the Four Color Theorem
10 tips for finding proofs
Open notebook mathematics
Alternate Perspective
Possible complaints/points off from your TA
Some common induction mistakes
Problem: Prove 2n n for all integers n 2 1.