1. Bartosz Naskręcki, ĐH Adam Mickiewicz, Ba Lan

Title: When Machines Prove Theorems: AI, Formalization, and the New Landscape of Mathematics

Abstract: Mathematics is, very quietly, going through one of the deepest transformations in its history. In the span of just a few years, we have learned to write mathematical proofs in a language that a computer can fully verify, to organize an entire shared library of modern mathematics — Mathlib — and to enlist large language models as collaborators that can suggest definitions, search for lemmas, and even close routine subgoals on their own.

In this one-hour lecture, aimed at the talented undergraduates of the VIASM REU, I will tell the story of how this came about and where it is going. We will look at concrete examples — from the formalization of deep theorems in number theory and combinatorics, to recent striking results in which AI systems have contributed to genuinely new mathematics — and we will see, in a live demonstration, what it actually looks like to work with Lean and an AI copilot side by side.

The talk will be accessible to any mathematically curious student. No background in logic, programming, or artificial intelligence is required; only an interest in mathematics and in the tools the next generation of mathematicians will be using. My hope is that you will leave the lecture not only better informed, but also tempted to try this yourself.

2. Phạm Hữu Tiệp, ĐH Rutgers, Mỹ