Posts
A small community of mathematicians is using a software program called Lean to build a new digital repository. They hope it represents the future of their field, explains Kevin Hartnett, senior writer at Quanta Magazine.
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.
Photo: Samuel Velasco/Quanta Magazine
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...
Buzzard, Massot and Commelin hoped to demonstrate that, at least in principle, Lean can handle the kind of mathematics that mathematicians really care about. “They’re taking something very sophisticated and recent, and showing it’s possible to work on these objects with a proof assistant,” Mahboubi said.
To define a perfectoid space, the three mathematicians had to combine more than 3,000 definitions of other mathematical objects and 30,000 connections between them. The definitions sprawled across many areas of math, from algebra to topology to geometry. The way they came together in the definition of a single object is a vivid illustration of the way math grows more complex over time — and of why it’s so important to lay the foundations of mathlib correctly.
Source: Quanta Magazine
