Lean è un assistente di verifica che aiuta i matematici a dimostrare i teoremi controllando il funzionamento e automatizzando alcuni dei passaggi di una prova. I matematici stanno traducendo la matematica in una forma che Lean può comprendere per digitalizzare la matematica, permettendo eventualmente ai computer di risolvere problemi aperti. Le persone che lavorano al progetto sperano che tra qualche anno sarà in grado di capire alcune domande negli esami di livello superiore.

Iscriviti al nosto canale Telegram, per le notizie in tempo reale!

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/