Hello to those people who are watching on video who can now actually hear me. Great.

Okay, back to topic. So post rigorous mathematics is what you do when you're a research mathematician,

which is you don't yet entirely know what the things are actually that you are talking

about. We don't have clear definitions of various things yet and so on and so forth.

That is not the kind of stuff that we can represent. But what instead we can represent,

which is not math, is for example various things in physics and these kinds of areas.

So the sciences that are close enough to mathematics to allow for unambiguous and to some extent

fully formal descriptions of the settings that these subjects talk about in the first

place that may also include things like biology. If you think about these taxonomic ontologies

and so on and so forth. So like I don't know a husky is a dog is a canine is a mammal is

a vertebrae is an animal and so on and so forth. These kinds of things of course we

can also represent. I'm not sure whether that counts as we can represent biology because

like large parts of biology are not just taxonomy. Yeah. Okay. Next up, what do we mean by knowledge?

Well in the area of mathematics that is relatively easy. Definitions, axiom statements, proofs

to some extent maybe notations and examples. But if you've seen pure math textbook at some

point you know this cliche of it's basically definition definition lemma proof lemma proof

theorem proof definition definition lemma proof theorem proof definition definition

definition right all of that stuff that we are interested in and those things we care

about representing such that we can do things with them on a computer. For example first

and foremost logical inference that includes things like automated and most importantly

interactive theorem proving interactive being more important because automated theorem proving

is very limited interactive theorem proving basically is not it's only limited by what

the person in front of the screen is willing to do in terms of work. IE things like the

modern theorem prover systems like lean cock formerly known as cock now named rock isabel

these kinds of systems and that is what we're interested in. But apart from things like

logical inference we can also do things like semantic search for which we don't necessarily

need to do any kind of fancy machine learning vector representation or whatever if we have proper

logical references of things we can actually do things precisely when it comes to search.

Similarly knowledge retrieval the things that potentially nowadays would power something like

a rag system and in particular these slides and these lecture notes that you're seeing right here

to some extent use exactly those principles which is why the layer system and so on and so forth

is an actual research project which we're working on. So all of the principles that you learn here

to some extent are realized in those very lecture notes which is why there are some words here

there are blue and if you hover over them nothing happens great right because they are in slides

mode. In notes mode it would show you a URI and then you could click on it and then you would end

up on the ILEA system which I'm going to show you later anyway. Okay which means if you take

this course you should have a working knowledge of first and foremost various mathematical

foundations. Why mathematical foundations? Because mathematical foundations are the things that make

precise what we talk about in mathematics in the first place and which we're going to use to

represent mathematical knowledge. That includes things like first-order logic, axiomatic set theory

expressed in first-order logic, higher-order logic, these kinds of things. Potentially logical

frameworks, Curry-Howard, these kinds of things. Okay you should also know their advantages and

disadvantages when it comes to actually implementing them on a computer because some of them are more

suitable for that than others with various trades off. So even though some of them might be better

suited to be implemented on a computer that might also mean that they're less suitable to be actually

used by working people with wet brains in their skulls. Various software applications.

Yeah disadvantages for software applications including things like automated and interactive

inference. Okay you should understand how to represent various kinds of mathematical settings,

groups, vector spaces, topological spaces, number spaces, all these kinds of things and various

advantages and disadvantages again of the various foundations for representing these kinds of things.