## Subtitles section Play video

• The following content is provided under a Creative

• Your support will help MIT OpenCourseWare

• To make a donation or view additional materials

• from hundreds of MIT courses, visit MIT OpenCourseWare

• at ocw.mit.edu.

• PROFESSOR: Now generally speaking,

• a proof is going to have seven characteristics

• that you want to keep in mind.

• Good proofs are correct-- that's obviously important--

• complete-- you've got to have all the details there.

• All of the key steps have to be there.

• They should be clear so we can understand what's going on.

• Brief is good.

• You don't want to crush somebody with all the details.

• You want to get to the key points, and be crisp.

• It's really nice if they're elegant.

• Now, that means clever.

• It's the mathematician's notion of beauty.

• Like you go to the art museum, and the artists will say,

• wow, that's a beautiful painting.

• In mathematics, you say, wow, that's an elegant proof.

• It's crisp, clever, short, to the point.

• And it's really the highest compliment

• you can get from a mathematician, anyway.

• And there's a lot of judgment that goes into that.

• Just like in art-- there's judgment

• over what is great art.

• The proof should be well organized.

• For example, use lemmas the same way

• you would use subroutines in writing

• code-- helps to make it clear.

• And the proof should be in order.

• Sometimes you'll see proofs where things are

• done in a haphazard fashion.

• All the pieces are there, but they're in the wrong order.

• Sometimes-- and they teach this in some high schools--

• they teach you to do proofs backwards.

• And the classic thing there is, say you're

• trying to prove a equals b.

• you're trying to prove.

• And then they'll do a bunch of steps.

• And then you'll end up with 1 equals 1,

• and you'll write a check, because you went

• from a equals b to 1 equals 1.

• And that's, of course, true.

• Now, that's not a good thing to do.

• It can be correct if the implications go this way.

• Because really, you're starting with a fact-- 1 equals 1--

• and deriving a equals b.

• So if, in fact, the implications work this way,

• then your proof is right.

• But most people, especially as you get farther along,

• think about it going from top to bottom.

• So don't use this technique, because it'll confuse people.

• You're liable to make a mistake.

• top down for being in order.

• Now, good proofs are very much like good code.

• In fact, one of the reasons we care so much about teaching you

• how to write a good proof in computer science

• is so that later on, you'll be able to prove

• that your programs are doing what you expect-- what they're

• supposed to do.

• Now, there are many famous examples where programs did not

• do what they were supposed to do,

• with disastrous consequences.

• The Airbus A300 was one of the first commercial jets totally

• operated by software.

• It could take off, fly, and land totally by software.

• It was a major advance in the airline industry.

• The only problem was, that on one

• of the first flights of the A300,

• the software accidentally opened the rear door just

• before landing.

• And the plane crashed as a result.

• It was the first plane crash in commercial history because

• of a software bug.

• There's a famous radiation device for cancer patients

• called the Therac-25.

• It's famous because it got into a race condition

• occasionally, which caused the device

• to just slam the patient with radiation-- so much so,

• it killed the patient.

• And they had multiple examples of this, and of course,

• a lot of lawsuits afterwards.

• How many of you all remember the 2000 election?

• A few of you do.

• OK, this will probably be the last class that remembers that.

• But that's where Al Gore was going up against George Bush--

• very close election-- all came down to recounting

• But in fact, Al Gore got negative 16,000 votes

• in one county because of a software bug

• in the electronic voting booths, which

• I think they got rid of a lot of them in the election

• after that.

• Because the software was buggy.

• and funny business in Florida.

• But getting negative 16,000 votes certainly

• didn't help his chances.

• Several years ago, a single faulty command

• in a computer system used by United and American Airlines

• grounded the entire fleets to both airlines for close

• to a day.

• Because they couldn't do anything.

• They're all run by computer, and the whole thing was screwed up.

• So there's lots more examples.

• We run into this issue all the time at Akamai.

• Akamai is a company started by MIT folks-- by myself,

• and Danny Lewin, and a dozen undergrads in the late 1990s.

• And we deliver a lot of the content

• you get on the web-- Facebook, all the search engines.

• A lot of the stuff you go to comes from our servers.

• So we've got to be very careful that we

• don't have software bugs.

• Now, in fact we do.

• And we catch them every once in awhile.

• But if we got a bad one, it would bring down

• all the sites you go to you.

• You wouldn't be able to go to those sites anymore.

• And everybody would notice.

• It would be sort of embarrassing.

• Now, this really does matter.

• And this is going to sound a little scary, but someday--

• probably 30, 20 years from now, somewhere

• in there-- it's possible that all of us, our lives

• may depend on the software that some of you write.

• In fact, to bring this home how scary it is,

• look at the person sitting next to you.

• And imagine that in 25 years, your life depends on

• whether their code does what it's

• supposed to do-- little scary.

• That's why we are very motivated to help

• you learn how to make rock-solid arguments,

• so you don't have code that fries one of your classmates

• someday, or puts him in a bad plane situation.

• Now unfortunately, writing rock-solid proofs

• is a very hard thing to do.

• Even the world's best mathematicians

• mess them up on a regular basis.

• In fact, it's estimated that one third of all published proofs

• have bugs, have flaws, that render the proof incorrect.

• The trouble often arises because we get lazy.

• We don't write down all the details or all the steps.

• Because, wow, it's clear.

• Let's just move on.

• Now, this can be OK.

• Not such a good practice, but it dramatically

• increases the chances of making a mistake.

• And there's some very famous examples

• in the math literature from the world's

• most famous mathematicians.

• Gauss-- and we'll talk about Gauss

• later during the term-- he's one of the most

• famous mathematicians ever.

• He wrote his PhD thesis in 1799.

• And it's usually referred to as the first rigorous proof

• of the fundamental theorem of algebra.

• And that says that every polynomial

• has a 0 over the complex numbers-- something

• probably a lot of you learned in high school.

• You get a polynomial.

• You can find roots of the polynomial

• over the complex numbers.

• But his thesis contains the following quote,

• "If a branch of an algebraic curve enters a bounded region,

• it must necessarily leave again.

• Nobody, to my knowledge, has ever doubted this fact."

• Warning signs-- buzzers-- should be going off in your brain.

• "But if anybody desires it, then on another occasion,