Speaker
Maurizio PAOLINI, Università Cattolica del Sacro Cuore
Abstract
I progressi recenti dell'intelligenza artificiale in campo matematico sono evidenti. In questo contesto LEAN si colloca come un interessante strumento per verificare formalmente dimostrazioni ottenute ad esempio con ChatGPT.
In realtà è molto di più: insieme alla libreria "mathlib" può essere uno strumento direttamente utilizzabile da un matematico. I progressi recenti autorizzano a pensare che nel giro di pochi anni si possa arrivare in molti ambiti della matematica ai confini della ricerca.
Verranno presentati dal vivo alcuni semplici esempi di utilizzo.
