đ The location of this session might change, please check here again before the session starts. The location is currently set to be next to Pixelebbe (Layer 2, G6). We will sit on the floor and won't have much space because we don't want to obstruct escape routes.đ
This session is for people who have some experience in proving, for instance because they are studying mathematics or a related field such as computer science or physics.
Constructive mathematics is a flavor of mathematics in which we use the axiom of choice and the technique of proof by contradiction only in certain special cases. The square root of two is constructively still irrational, but there might be vector spaces without a basis.
As a result, proofs are more informative (for instance regarding bounds), finer distinctions can be made (for instance between positive existence and mere impossibility of non-existence) and results apply more generally: Every constructive result also has a geometric interpretation, where it applies to continuous families, and an algorithmic interpretation, yielding computational witnesses such as procedures for computing the objects whose existence has been shown.
Relinquishing the axiom of choice and the principle of excluded middle also allows us to explore axioms and notions which are incompatible with these classical laws, such as mathematical settings in which all functions are continuous or in which the intuitive idea of a âgeneric ringâ can be put on a firm basis.