Mathematical Proof Is a Social Compact

“In 2012, the mathematician Shinichi Mochizuki claimed he had solved the abc conjecture, a major open question in number theory about the relationship between addition and multiplication. There was just one problem: His proof, which was more than 500 pages long, was completely impenetrable. It relied on a snarl of new definitions, notation, and theories that nearly all mathematicians found impossible to make sense of.”

“Years later, when two mathematicians translated large parts of the proof into more familiar terms, they pointed to what one called a “serious, unfixable gap” in its logic — only for Mochizuki to reject their argument on the basis that they’d simply failed to understand his work.”

“What is a mathematical proof?”

“Andrew Granville, a mathematician at the University of Montreal”

“Last month, one of his papers on “how we arrive at our truths” was published in the Annals of Mathematics and Philosophy.”

“People tend to see mathematics as this pure quest, where we just arrive at great truths by pure thought alone. But mathematics is about guesses — often wrong guesses. It’s an experimental process. We learn in stages.”

“The culture of mathematics is all about proof. We sit around and think, and 95% of what we do is proof. A lot of the understanding we gain is from struggling with proofs and interpreting the issues that come up when we struggle with them.”

“The main point of a proof is to persuade the reader of the truth of an assertion. That means verification is key.”

“The best verification system we have in mathematics is that lots of people look at a proof from different perspectives, and it fits well in a context that they know and believe.”

“Mochizuki did not want to play the game in the way it’s played. He has made this choice to be obscure. When people make big breakthroughs, with really new and difficult ideas, I feel it’s incumbent on them to try and include other people by explaining their ideas in as accessible a way as possible.”

“And he was more like, well, if you don’t want to read it the way I wrote it, that’s not my problem. He has the right to play the game he wants to play. But it’s nothing to do with community. It’s nothing to do with the ways that we make progress.”

“there were problems with the axiomatic system.”

“Russell and Alfred Whitehead tried to create a new system of doing math that could avoid all these problems. But it was ludicrously complicated, and it was hard to believe that these were the right primitives to start from. Nobody was comfortable with it.”

“David Hilbert came along and had this amazing idea: that maybe we shouldn’t be telling anyone what’s the right thing to start with at all. Instead, anything that works — a starting point that’s simple, coherent and consistent — is worth exploring.”

“Hilbert didn’t start off doing this for abstract reasons. He was very interested in different notions of geometry: non-Euclidean geometry. It was very controversial. People at the time were like, if you give me this definition of a line that goes around the corners of a box, why on earth should I listen to you? And Hilbert said that if he could make it coherent and consistent, you should listen, because this may be another geometry that we need to understand. And this change in viewpoint — that you can allow any axiomatic system — didn’t just apply to geometry; it applied to all of mathematics.”

“some things are more useful than others. So most of us work with the same 10 axioms, a system called ZFC.”

“We continue with this sort of plurality. It’s not clear what’s right, what’s wrong. According to Kurt Gödel, we still need to make choices based on taste, and we hopefully have good taste. We should do things that make sense. And we do.”

“To discuss mathematics, you need a language, and a set of rules to follow in that language. In the 1930s, Gödel proved that no matter how you select your language, there are always statements in that language that are true but that can’t be proved from your starting axioms.”

“you have this philosophical dilemma immediately: What is a true statement if you can’t justify it? It’s crazy.”

“Professional mathematicians largely ignore this. We focus on what’s doable. As Peter Sarnak likes to say, “We’re working people.” We get on and try to prove what we can.”

“Now people say, oh, we’ve got this computer, it can do things people can’t. But can it? Can it actually do things people can’t? Back in the 1950s, Alan Turing said that a computer is designed to do what humans can do, just faster. Not much has changed.”

“You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on.”

“ChatGPT and other machine learning programs are not thinking. They are using word associations based on many examples. So it seems unlikely that they will transcend their training data.”

“There’s a robustness, a health, in how different communities come together to work on and understand a proof. If we’re going to have computer assistance in mathematics, we need to enrich it in the same way.”