Quanta Magazine: Building the Mathematical Library of the Future

Quanta Magazine: Building the Mathematical Library of the Future. “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. But first, the mathematicians who gather on Zulip must furnish Lean with what amounts to a library of undergraduate math knowledge, and they’re only about halfway there.”

Leave a Reply