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)