Embracing AI and Formalization: Experimenting with tomorrow's mathematical tools

Lunedì 2 dicembre 2024, alle ore 16.00, presso il Dipartimento di Matematica e Fisica (Aula M1 - Lungotevere Dante 376), si terrà il prossimo Colloquium di Matematica del prof. Jarod Alper (University of Washington) dal titolo "Embracing AI and Formalization: Experimenting with tomorrow's mathematical tools".

Abstract:

Si dice che l'intelligenza artificiale e la formalizzazione rivoluzioneranno la matematica, i computer supereranno presto gli esseri umani nella risoluzione di problemi. Non più ricerca per la dimostrazione dei teoremi, ma guida dei computer che produrranno dimostrazioni per noi. Come può un giovane matematico in carriera prepararsi per affrontare le sfide della matematica del futuro? Dovrà apprendere le tecniche Lean o machine learning?

Il prof. Alper ci racconterà la sua personale esperienza di come si è avvicinato all'A.I. applicata alla formalizzazione in matematica, attraverso l'eXperimental Lean Lab (XLL) presso l'Università di Washington.

You've heard the buzz: AI and formalization will revolutionize mathematics. Computers will soon surpass humans in solving olympiad-style problems. Humans will transition from proving research-level theorems on their own to guiding computers. And maybe you even believe the hype. Other than pulling out your hair waiting for the day when computers take your job, what can you do? If you are like most career mathematicians, you are already overwhelmed with too many academic responsibilities, reserving any precious spare work hours for research. Where are you going to find the time to learn Lean or machine learning techniques?

While I don't have the answers, I can share how I have embraced the potential of AI and formalization in mathematics through the eXperimental Lean Lab (XLL) at the University of Washington. I hope to inspire you to also get involved and play an active role in guiding the transformation of our field.

Locandina