The Colloquium is today (Thursday) November 9th, 2023 from 4PM ____________________________________________________________________
125. matematicke kolokvium:
WHAT IS THE ROLE PROOF PLAYS IN PURE MATHEMATICAL RESEARCH AND WILL AI CHANGE THAT?
A. Granville
ctvrtek 9. listopadu 2023 v 16:00, poslucharna S5, druhe patro
MFF UK, Malostranske nam. 25, Praha 1 ____________________________________________________________________
Abstract. We largely understand mathematics by how we develop proofs, in particular the issues that arise as we understand enough, in detail, to construct a proof. Computer assistance in cutting-edge proofs is now a reality. At the moment its role is small -- helping unsure authors verify that they have not overlooked an issue in a complicated proof, but it is not difficult to predict that this is just the start. For example computers might soon play a more prominent role, for example by filling in the details from a basic plan, efficiently finding out how to make the details work. Then what? As our role is diminished, what becomes the function of a research mathematician? In this lecture we will start from Aristotle's suggestion of building understanding from ``primitives'', and survey how mathematicians traditionally function today. We will then discuss some of the developments with computer assistance, particularly Lean, and what will happen with that in the foreseeable future. One goal is to discuss the question ``If Lean tells you that a proof is correct, what should you believe?'' ____________________________________________________________________
(pdf pozvanky - obsahuje laudatio, fotografii a dalsi informace o kolokviich: https://kam.mff.cuni.cz/~klazar/granville.pdf)