Okay, the quiz is over.

Okay, there's possibly something wrong.

When you can look at the quiz, whenever there is kind of this situation that nobody got,

there's truths about proofs in this case.

There may be an error in the quiz.

So if you think you have an error, you see an error in the quiz, please tell us.

And then we'll disregard that or try to re-grade or something like this.

Okay, so we've talked about how to do mathematical proofs.

Mathematical proofs are at the center of symbolic AI because anything we do we have to prove.

And the good thing is we can actually prove many things.

Think of proofs as the ultimate explanations.

They can convince you why certain things are true, not only that they're true.

And the last thing we looked at was essentially I tried to convince you that even though we have this very nice and low-level language of the things you're allowed to do in a proof,

that is not how we do things in practice because these things that you're allowed to do in a proof is so detailed, so boring and tedious that nobody does it.

We all believe that it's possible in principle,

but we kind of play proving like a social game, right, where you have somebody who tries to prove something, the proponent,

and there are a couple of things a proponent can do, like claim things and justify things and all of those kind of things.

And we have an opponent because if you can just claim something is true and you don't have an opponent, the game is no fun, right?

And the opponent can challenge. Try to shoot the ideas down.

And the idea is that if you try to shoot the ideas down and you just don't succeed and you've really tried, then the proof is watertight,

even though it's not at this level of the things you can do when you write down the proof.

That's just a social efficiency measure.

And the proof, as we see it, say, in the slides or in a journal paper in mathematics or computer science,

is kind of at a level where between the level of the proof typically and the level of this fully explicit proof,

there's a factor of a hundred or so, possibly a million or whatever.

Okay? It really depends on how detailed the proofs are is what we expect of our audience.

When I show a proof to you, I give a lot more detail than when I show it to my colleagues.

Okay. Any questions to this?

So I've already told you about this.

I'm not quite sure about this section of whether you would rather learn this by osmosis as you do it in every other course that I know,

or being told about the methods as they are.

Okay. I'd like feedback.

What I would like you to do is to kind of keep open your eyes in all of your courses of what's really happening right now, right?

In terms of the language.

Because you need to learn this language.

Whether I...

Whether we kind of teach it to you, like French in school or something like that,

or we just dump you in a French kindergarten or something like this.

The way to learn French or German or Chinese or so.

I've tried to do the teach method.

Okay. There's one more thing.

In math, we love to give names to things that I already told you.

That are one letter long.

Because it allows us to say a lot in very little space.

So there's A, B, C, D, E, X, Y, Z, all these letters in capital and lowercase.

And that's nice. But not enough.

So I'm sure you've seen this.

We use Greek letters because they're sufficiently different.

Most of them.

And so you will either have to have learned the Greek alphabet or you still need to learn it.