Philosophy of Mathematics Seminar (Monday - Week 2, HT26)

Abstract: A formalist might describe mathematics as a way of making logical deductions about numbers, shapes, symmetry etc via manipulation of symbols according to precise logical rules. A working mathematician typically has a completely different view of the subject. However in recent years computer theorem provers such as Lean (which work formally) have been used to check results in modern research mathematics, and in the last two months AI agents wrote Lean code resolving open problems raised by Erdős (a high-profile mathematician who made progress partly by asking good questions). Mathematicians are for the most part in denial about all of this — but will formalization change the way mathematics is done? I will give a background to the area and survey the facts.

Please note: A notice will be sent out for each talk with the Zoom link.