GoKawiilBecause of this, previous attempts to digitize mathematical results (such as a 1994 project called the QED Manifesto) quickly deteriorated into arguments about which definitions and frameworks to use. “Everybody loves this idea in principle, but in practice, it’s a nightmare,” Dick said. “They disagree about what programming language to write in. … There’s fundamental disagreement about whether this kind of project could be possible at all.”
To avoid these disagreements, a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library and how those definitions should be coded — much as Wikipedia does it, according to Simon DeDeo of Carnegie Mellon University.
“It is really a community trying to do the best thing for the community,” said Emily Riehl, a mathematician at Johns Hopkins University. So far, it’s worked, and the process has been largely democratic. But, she said, “what’s bad about it is, there is one decision that will be made in the end, [when] in many cases, there’s not one correct decision. Some people will be happy, and other people will be unhappy.”
Just as Bourbaki’s approach was optimal for certain subjects and not others, the Lean language and the choice of definitions that go into its library are better suited to some areas of math than others. They’re a good fit for number theory and algebraic geometry, for instance. Graph theory and category theory, not so much.
This is just one way Lean could make math more homogeneous. Dick points out that past technologies — even choices of which notation to use — have subtly changed how mathematicians approach their work. Lean might encourage them to focus on developing concepts that can be formalized more easily, even if they don’t realize it. “I’ve now found so many cases where something like that is happening,” she said — where “it actually shifts the focus and the intuition and the understanding away from the mathematical problem domain toward the behavior of this system.”
There is certainly a lot to be excited about when it comes to Lean. But Riehl, for her part, thinks that mathematicians should try to use more than one kind of proof assistant, rather than relying solely on Lean. She’s not sure how practical that will be, however, given how much effort formalization requires.
On Overcorrection
For centuries now, mathematicians have sought greater rigor by focusing on whether they can verify every line of a proof. But that wasn’t always the case. To Descartes in the 1600s, rigor meant being able to hold an idea in your head and intuitively understand why it’s true. As a result, according to Akshay Venkatesh of the Institute for Advanced Study, older proofs used to “have a kind of grittiness.”
“It doesn’t make for a formally elegant argument,” he said. But it’s “something a human being can easily understand.” Modern proofs are more elegant, sure. But they’re also more slippery, harder for the mind to get a grip on. (Interestingly, Buzzard used similar language while discussing his hopes for how Lean would influence proof-writing. “I want this argument to be a thing of beauty,” he said. “I want it to slip down the throat.”)
This trend reflects a notion that’s now taken for granted: that proof should lie at the heart of math. “There’s no question that the concept of proof is a fundamental part of mathematics,” Venkatesh said. But “where I think there should be a question is whether it should be the defining feature of mathematics.”
... continue reading