Original subtitles

What about that other classic AI stuff? We talked about theorem proving,

can we prove mathematical theorems. That stuff is happening too and it's also important.

So, on the logic front for example we can build amazing theorem provers

compared to when people started doing this. These provers are used for

more than just proving theorems. For example, NASA uses these for fault diagnosis.

There are some question answering systems which are no longer

purely logical, but there is a component of logical theorem proving. You try to

prove that the statement

that you think answers the question actually entails the question in the appropriate way.

That's the way that logic and theorem proving has made its way into very different

domains like natural language processing. The methods people use are things like

deduction systems. The closest we'll get to this in this class is constraint satisfaction,

but you'll get a flavor for how this stuff works.

Also it's worth pointing out that satisfiability solvers have had

huge advances in the past decade and are now able to do really amazing things.

What's shown here on the right is a proof of something called the Robbin's conjecture.

You probably

haven't heard the Robbin's conjecture itself, but it was an open algebraic question,

and there is a short, human interpretable proof

that a theorem prover chugged out that humans have been looking for for a while. This is a case of

you see it, and you're like, yeah, that's right.

That's a case of an open question being proved by a computer in the way

humans would prove it, in the sense that the human can interpret the proof.

There's also theorem proving by computers where the computer does a brute force,

where human doesn't want to check 4.7 billion cases, but the computer does,

and so the computer does it.