Abstract: In this lecture, I will give an introduction to toric varieties and cones, and propositions and relations about them.

Abstract:

Abstract: The classical understanding of logic and, by extension, of mathematics is based upon the notion of truth. In that view, the role of a mathematical proof is to establish the truth of some statement, at which point the proof itself can be discarded. For instance, when computing a derivative, we apply the chain rule, not its proof.

Constructive mathematics reverses this approach, focusing primarily on the notion of a proof itself. It asks that all proofs be effective, thus rejecting classical principles such as the law of excluded middle. Initially seen as a largely philosophical position, constructive mathematics has come back to the forefront, since it is precisely the kind of mathematics that computers can understand.

In this talk, we will explore the main principles of constructive mathematics as developed by early constructivists: Brouwer and Heyting, and see how it is used these days by mathematicians around the world who wish to verify the correctness of their proofs using computers.