I will discuss the renewed value of formalization in the era of Math 2.0, and the role the enterprise can play in helping align AI with mathematical practice. On the way, I will sketch some of the essential ideas underlying modern theorem provers (including LEAN), and underline the potential problems and pitfalls raised by autoformalization.

(15 min presentation + 30 min discussion)

What is the best way of using AI in mathematical research? What kind of AI models should be made available to members of the department, and how can we make the best use of them?

(15 min presentation + 30 min discussion)

What should we value in mathematical research in the age of AI? How should we adapt our criteria for assessing originality, creativity, and scientific contributions?

Hugo Tavares (15 min) + PhD student (15 min, TBC) + 30 min discussion

How should we adapt the supervision and training of MSc students, PhD students, and postdoctoral researchers?