15-251: Great Theoretical Ideas in Computer Science Lecture 4

On Proofs*

2. 1.

What is a proof? How do I find a proof?

3. How do I write a proof?

My philosophy for math problems:

2. 1. What is a proof? How do I find a proof?

3. How do I write a proof?

Make 1% progress per day, for 100 days.

251 HMWK version: 15% progress per day for 7 days.

nd it looks ve done e the idea will work ng out; mall trick better but I play with er a while, I ng on.

I don't have any magical ability. When I was a kid, I had a romanticized notion of mathematics, that hard problems were solved in 'Eureka' moments of inspiration. [But] with me, it's always, 'Let's try this. That gets me part of the way, or that doesn't work. Now let's try this. Oh, there's a little shortcut here.' You work on it long enough and you happen to make progress towards a hard problem by a back door at some point. At the end, it's usually, 'Oh, I've solved the problem.'

10 tips for finding proofs

1. Read and understand the problem. 2. Try small cases. n = 1? n = 2? 3. Develop good notation.

Terry Tao
(Fields Medalist, MacArthur Genius, winner of 10+ international math prizes worth $2,000,000)

4. Put yourself in the mind of the adversary. 5. Clarify, abstract out, summarize pieces.

10 tips for finding proofs

6. Use blocks of 1 hour. 7. Take breaks. 8. Use plenty of paper, and draw pictures. 9. Collaborate. 10. I couldnt think of a 10th one.

251 Homework Problem, Spring 2010:

The kitchen for a cookie baking contest is arranged in an m by n grid of ovens. Each contestant is assigned an oven and told to make as many cookies as possible in three hours. Prizes are awarded in the following manner: in each row the p people who produced the most cookies receive a prize. Likewise, in each column the q people who produced the most cookies receive a prize. Assume p n, q m, and that no two people produced the same number of cookies. Prove that at least pq people received two prizes for their cookiebaking performance.

Small cases p = 1, q = 1 p = 2, q = 1 Simplified notation p = 3, q = 1 Consolidated q = 1, general p

experimenting with p = 2, q = 2 being the adversary: what are the worst cases? Lucked into some good notation decided to try induction

induction doesnt quite lead to a smaller version of the same problem strengthen induction hypothesis? using lots of paper, at least

take a break

figured out strengthened induction hypothesis that seems to work read the problem carefully to check that base case okay

consolidate proof sketch so I dont forget

LaTeXing it up

If you just read the solution, its frustrating: Writeup is short: 3 paras, < -page. Seems to have some aha! moments. Most of the cognitive process is missing.

Open notebook mathematics

Polymath project:
http://gowers.wordpress.com/category/polymath1/

Gauss Gauss: the ultimate jerk

Sir Tim Gowers (Fields Medalist)

What is a proof?
In math, there are agreed-upon rigorous rules of deduction. Proofs are right or wrong. Nevertheless, what constitutes an acceptable proof is a social construction. (But computer science can help.)

2. 1.

What is a proof? How do I find a proof?

3. How do I write a proof?

Proofs prehistory

Proofs 19th century

Euclids Elements (ca. 300 BCE)

True rigor developed. Culminated in the understanding that math proofs can be formalized with First Order Logic.

Canonized the idea of giving a rigorous, axiomatic deduction for all theorems.

It became generally agreed that you could rigorously formalize mathematical proofs. Bertrand Russell Alfred Whitehead But nobody wants to!
(by hand, at least)

Principia Mathematica, ca. 1912 Developed set theory, number theory, some real analysis using formal logic. page 379: 1+1=2

But are English-language proofs sufficient?

Four Color Theorem

1852 conjecture: Any 2-d map of regions can be colored with 4 colors so that no adjacent countries get the same color.

Four Color Theorem

1879: Proved by Kempe in Amer. J. of Math 1880: Alternate proof by Tait in Trans. Roy. Soc. Edinburgh 1890: Heawood finds a bug in Kempes proof. 1891: Petersen finds a bug in Taits proof. Kempes proof was widely acclaimed.

Four Color Theorem

1969: Heesch showed that the theorem could in principle be reduced to checking a large number of cases.

Four Color Theorem

Much controversy at the time. Is this a proof?? Arguments against:
No human could ever hand-check the cases. Perhaps theres a bug in the code. Perhaps theres a bug in the compiler. Perhaps theres a bug in the hardware. No insight is derived still dont know why the theorem is true.

1976: Appel and Haken wrote a massive amount of code to compute and then check 1936 cases (1200 hours of computer time). Claimed this constituted a proof.

Nevertheless, these days, pretty much everyone credits Appel & Haken with the proof.

Four Color Theorem

A&H found, classified various errors in their work. Type 1: few minute fix. Type 3: few day fix. Ulrich Schmidt 1980 masters thesis: found thirteen Type 1 errors, one Type 3. A&H fixed them all (?) in a 1989 book. 1997: Simpler computer proof by Robertson, Sanders, Seymour, Thomas.

Classification of finite simple groups

(the prime numbers of group theory) Theorem: Every finite simple group is either Relevance: Our fastest graph isomorphism alg. Progress started in late 19th century. 100s of papers, 10,00020,000 pages later 1983: Gorenstein announces proof is complete. However, experts knew one piece still missing. 2004: Aschbacher & Smith finish a 1221-page paper, Aschbacher announces proof is complete.

Classification of finite simple groups

Some controversy: Is the theorem proven? Genuine concern: Everyone who understands the proof will die before its properly collated. (The youngest person who knows the proof?) Inna Capdeboscq: 1993: 1994:

More anecdotes
Wiles announces proof of FLT. Then a bug is found. Bug fixed, 100-page paper.

1994: Gaoyong Zhang, Annals of Mathematics: proves n=4 case of Busemann-Petty. 1999: Gaoyong Zhang, Annals of Mathematics: disproves n=4 case of Busemann-Petty.

A ~5000 page, 13-volume series of books describing the proof is underway.

Kepler Conjecture
2005: Kepler, 1611: As a New Years present (???) for his friend, wrote a paper with this conjecture: The densest way to pack spheres is like this:

Kepler Conjecture
Our neighbor Tom Hales: 120 page proof in Annals of Mathematics Plus code to solve 100,000 distinct optimization problems, taking 2000 hours computer time. Annals recruited a team of 20 referees. They worked for 4 years. Some quit. Some retired. One died. In the end, they gave up. But said they were 99% sure it was a proof.

Kepler Conjecture

Computer-assisted proof
Proof assistant software like HOL Light, Mizar, Coq, Isabelle, does two things:

Hales: I will code up a completely formal axiomatic proof, checkable by computer. Open source Project Flyspeck: 200420??

1. Checks that a proof encoded in an axiomatic system for First Order Logic (or typed lambda calculus theory) is valid. 2. Helps user code up such proofs. Developing proof assistants is an active area of research, particularly at CMU!

Computer-assisted proof
Suppose, e.g., HOL Light certifies a formal proof. Can you trust it? You dont need to trust the million-line proof. You dont need to trust the process used to generate that proof. You just need to trust HOL Lights 430-line program for verifying FOL deductions.

Computer-formalized proofs
Fundamental Theorem of Calculus (Harrison) Fundamental Theorem of Algebra (Milewski) Prime Number Theorem (Avigad++ @ CMU) Gdels Incompleteness Theorem (Shankar) Jordan Curve Theorem (Hales) Brouwer Fixed Point Theorem (Harrison) Four Color Theorem (Gonthier) Feit-Thompson Theorem (Gonthier, 4 months ago)

Proof of the Four Color Theorem

Variable R : real_model. Theorem four_color : (m : (map R)) (simple_map m) -> (map_colorable (4) m). Proof. Exact (compactness_extension four_color_finite). Qed. + about 60,000 more lines

2. 1.

What is a proof? How do I find a proof?

3. How do I write a proof? So as to get full points on the homework.

Your homework is not like the Four Color Theorem. The TAs can correctly decide if you have written a valid proof.

Here is the mindset you must have.

Pretend that your TA is going to code up a formalized proof of your solution. Your job is to write a complete English-language spec for your TA.

You must give a spec to your TA that they could implement with no complaints or questions.

program manager

You:

Your TA:
developer

Equivalently, you must convince your TA that you know a complete, correct proof.

Alternate Perspective

Possible complaints/points off from your TA: A does not logically follow from B. You missed a case. This statement is true, but you havent justified it. But also: I dont understand your proof.

You: must present an airtight case.

Your TA

This explanation is unclear. Your proof is very hard to read.

TA

Questions?

Problem: Solution:

Prove n2 n for all integers n.

Some common induction mistakes

The base case F0 is true because []. For the induction step, assume Fk holds for all k. We now show that Fk+1 holds You just assumed what youre trying to prove! The proof is by strong induction. The base case F0 is true because [] For the induction, assume Fk holds for all k n. We will now show Fk+1: [] What is k? Where did n go?

We prove Fn = n2 n by induction on n. The base case is n = 0: indeed, 02 0. Assume Fn. Then (n+1)2 = n2+2n+1 n2+1 n+1 (by Fn). This is Fn+1, so the induction is complete.

Read the question carefully.

Spring 11 homework 2, #2a: How many ways to arrange c 0 s and d 0 s so that all s are consecutive? Solution:
You can have any number between 0 and d s, then the string of s; then you must have the remainder of the s. Hence there are d+1 possibilities.

Problem: Solution:

Prove 2n > n for all integers n 1.

Fn = 2n > n F1 = 2 > 1 Fn Fn+1: 2n+1 = 22n > 2n (induction) n+1 because n 1 Therefore proved. This is not a full sentence.

Fallacious if c = 0: there is only 1 possibility.

Handle all edge cases! Dont have any missing parts in your spec.

This is not written in English!

Spring 11 homework 2, #3a: There is a circle of 15,251 chips, green on one side, red on the other. Initially all show the green side. In one step you may take any four consecutive chips and flip them. Is it possible to get all of the chips showing red? Intended solution: No. In flipping 4 chips, if g of them are green, then after flipping 4g of them are green. Note that g and 4g have the same parity; hence the parity of the number of green chips will always remain odd.

Solution: No it is not possible. Lets assume for contradiction we converted all 15,251 chips to red. But this means in the very last step there must be 4 consecutive green chips and the remaining 15,247 must be red. Repeating this k times for 1 k 3812, we get three consecutive red chips, with the rest green. But we started from all green, contradiction. If asked to show something is impossible, it does not suffice to show that one particular method does not work.

Spring 11 homework 2, #3b: There is a circle of 15,251 chips, green on one side, red on the other. Initially all show the green side. In one step you may take any seven consecutive chips and flip them. Is it possible to get all of the chips showing red? Intended solution: Yes. Number the chips 015,250. Flip the sequence [0,1,,6], then [1,2,,7], then [2,3, ,8], etc., up until [15,250,0,1, ,5]. Now each chips been flipped exactly 7 times, an odd number. Hence each chip is now red.

Solution: At any given time, let g be the number of chips showing green and r the number of chips showing red. The possible remainders when a number is divided by 7 are 0, 1, 2, 3, 4, 5, 6, 7. A flip that involves 6 red and 1 green increments the current modular class of g by 5 while the move that involves 1 red and 6 green decrements the current modular class of g by 5. Originally, with the number 15,251, the modular class of g mod 7 is 5. Thus, it is possible to make all chips red. Wut.

Solution: At any given time, let g be the number of chips showing green and r the number of chips showing red. The possible remainders when a number is divided by 7 are 0, 1, 2, 3, 4, 5, 6, 7. A flip that involves 6 red and 1 green increments the current modular class of g by 5 while the move that involves 1 red and 6 green decrements the current modular class of g by 5. Originally, with the number 15,251, the modular class of g mod 7 is 5. Thus, it is possible to make all chips red. In short: this proof does not make sense. Do not just write a bunch of random facts.

Solving problems: try small cases use enough time & paper put yourself in the mind of adversary Writing proofs: like designing a complete, correct spec put yourself in the TAs shoes use good English!

Study Guide

10