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

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.

This talk is an overview of a genre of theorems called "Grothendieck-Lefschetz theorems". I will start by introducing Lefschetz's original theorem. Our next, stop is Grothendieck's theorem for divisors and line bundles which can be though of as a codimension one Lefschetz theorem in the algebraic category.

From this point there are two natural paths to generalisation. The first is to higher codimension subvarieties. In this direction there are some infinitesimal results due to Girivaru-Patel.

The second path considers higher rank bundles. The first results in this direction are due to Hartshorne. In joint work with R. Girivaru, Hartshorne's work has been generalised to principal bundles. The talk will end with some applications of our result to splitting criteria.

Informally, if two functions can be “continuously deformed” from one to the other, this is called a homotopy. Homotopy emerged from theory more than a century ago and was introduced as a numerical method for solving non-linear problems in the 1960s. The basic components of these early continuation algorithms built on earlier path-tracking methods, which exist in today’s “black box” solvers. We will look at the building blocks of continuation algorithms, how they work (or don’t), and how key insights from the 1970s and 1980s contributed to some powerful polynomial-solving software packages.