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

Dr Bartosz Naskręcki is a graduate of Adam Mickiewicz University and specializes in number theory and algebraic geometry. After obtaining his doctorate in 2014, he completed several years of research internships in Bayreuth, Bavaria, Bristol, UK, and at the Dioscuri TDA Center in Warsaw. For over four years, he has been collaborating with Prof. Mariusz Jaskólski in the field of mathematical crystallography, which culminated in a sectional lecture at the European Crystallography Congress ECM 2025. In 2022 and 2023, he received the Crystallography Diamonds award twice, granted by the Crystallography Committee of the Polish Academy of Sciences.

In 2025, he co-created the most difficult mathematical test for LLMs, the FrontierMath project. His mathematical problem was included in the most difficult variant of this Tier 4 test, which has so far resisted all the most powerful language models.

He is passionate about teaching students at the intersection of computer science and mathematics, teaching courses in areas such as cryptography, mathematical computing in Python, and the use of large language models in mathematical and programming work. He is interested in all aspects of the use of computers in groundbreaking mathematical work.

Dr. Bartosz Naskręcki is also an active popularizer of knowledge, especially regarding the contribution of Polish cryptologists to breaking the Enigma machine code. He received the Polish Mathematical Society's award for young mathematicians for 2013, and in 2010 he was honored in the Józef Marcinkiewicz Competition for the best student work in mathematics.

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ỹ

Short bio: Pham Huu Tiep graduated from the Chu Van An High School, Hanoi, in 1979. He was a member of the Vietnam team at the IMO 1979 in London, UK, winning a silver medal. In 1980, he entered Moscow State University (Moscow, Russia), where he subsequently obtained a Ph. D. degree in 1989 and a D. Sc. degree in 1991. He was on the faculty of University of Florida, University of Arizona, and is currently Joshua Barlaz Distinguished Professor at Rutgers University, USA.

Tiep works mainly in group theory and representation theory. He was an invited speaker at the 2018 International Congress of Mathematicians in Rio de Janeiro, Brazil, and also gave plenary addresses at meetings of the American Mathematical Society and the Canadian Mathematical Society. He is a Fellow of the AMS, Clay Senior Scholar, Simons Fellow, and has published 5 books and more than 200 research papers