You can think of a proof as a social compact — a sort of mutual agreement between the author and their mathematical community. We’ve seen an extreme example of this not working, with Mochizuki’s claimed proof of the abc conjecture.
And I should say, 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.
But of course, some things are more useful than others. So most of us work with the same 10 axioms, a system called ZFC.
Which leads to the question of what can and can’t be deduced from it. There are statements, like the continuum hypothesis, which cannot be proved using ZFC. There must be an 11th axiom. And you can resolve it either way, because you can choose your axiomatic system. It’s pretty cool. 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.
Speaking of Gödel, he plays a pretty big role here, too.
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. It’s actually more complicated than that, but still, you have this philosophical dilemma immediately: What is a true statement if you can’t justify it? It’s crazy.
So there’s a big mess. We are limited in what we can do.
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.
https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/
Know Thyself 