Constructive and Computational Mathematics

Constructive mathematics began from the both philosophical and practical idea that proofs should have *computational content*: for instance, a proof of existence of some object should yield, directly or indirectly, a construction of the desired object. Today, this has been more or less realised in various areas of mathematics, and the proofs are in many cases implemented on computers.

This course will give an introduction to the modern constructive development of algebra, analysis, and topology (with a little logic on the side), with an emphasis on the computational interpretations. In the constructive development of topology, point-free methods — based on Grothendieck’s generalised topologies — are crucial.

No logical background is required. The only prerequisites assumed will be general advanced-level courses in algebra, topology and analysis, as included in the typical MSc background.

First meeting: Tuesday 23 Jan, 14:00–15:00 (venue TBA); further schedule to be agreed on at that meeting.

Intended audience: Ph.D. students and masters students with interest in logic or computer implementation of mathematics.