When you see “2 + 2 = 4”, what does “=” mean? It turns out that’s a complicated question, because mathematicians can’t agree on the definition of what makes two things equal. While this argument has been quietly simmering for decades, a recent push to make mathematical proofs checkable by computer programs, called formalisation, has given the argument new significance.
“Mathematicians use equality to mean two different things, and I was fine with that,” says Kevin Buzzard at Imperial…