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. Lean won’t be solving open problems anytime soon, but the people working on it are almost certain that in a few years the program will at least be able to understand the questions on a senior-year final exam.
More on Lean and the future of mathematics below
Comments