The Effort to Build the Mathematical Library of the Future

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. Original story reprinted with permission from Quanta Magazine, an editorially independent publication of the Simons Foundation whose mission is to enhance public understanding of science by covering research develop ments and trends in mathe matics and the physical and life sciences. 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.