quantummagazine | Every day, dozens of like-minded mathematicians gather on an online forum called Zulip to build what they believe is the future of their field.
They’re all devotees of a software program called Lean. It’s a “proof assistant” that, in principle, can help mathematicians write proofs. But before Lean can do that, mathematicians themselves have to manually input mathematics into the program, translating thousands of years of accumulated knowledge into a form Lean can understand.
To many of the people involved, the virtues of the effort are nearly self-evident.
“It’s just fundamentally obvious that when you digitize something you can use it in new ways,” said Kevin Buzzard of Imperial College London. “We’re going to digitize mathematics and it’s going to make it better.”
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.
And after that, who knows? The mathematicians participating in these efforts don’t fully anticipate what digital mathematics will be good for.
“We don’t really know where we’re headed,” said Sébastien Gouëzel of the University of Rennes.
0 comments:
Post a Comment