Building the Mathematical Library of the Future | Quanta Magazine
peter.suber's bookmarks 2020-10-24
"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...."