Pizza Seminar
Speaker: Chris Kapulkin (Western)
"An invitation to constructive mathematics"
Time: 17:00
Room: MC 107
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.