Building the Mathematical Library of the Future | Quanta Magazine

peter.suber's bookmarks 2020-10-24

Summary:

"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...."

Link:

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/

From feeds:

Open Access Tracking Project (OATP) » peter.suber's bookmarks

Tags:

oa.new oa.mathematics oa.floss oa.repositories oa.tools oa.digitization oa.ai

Date tagged:

10/24/2020, 10:01

Date published:

10/24/2020, 06:01