Building the Mathematical Library of the Future

Kevin Hartnett, Senior Writer. Quantamagazine
Event type

"A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field."


"Digitizing mathematics is a longtime dream. The expected benefits range from the mundane — computers grading students’ homework — to the transcendent: using artificial intelligence to discover new mathematics and find new solutions to old problems. Mathematicians expect that proof assistants could also review journal submissions, finding errors that human reviewers occasionally miss, and handle the tedious technical work that goes into filling in all the details of a proof."