Mathematician Explains Equals Has Multiple Meanings

Mathematics has many abstract concepts that are often difficult to grasp, but we assumed the meaning of ‘equals’ was well understood. However, it appears that mathematicians disagree on the exact definition of equality, which could pose challenges for computer programs increasingly used to verify mathematical proofs.

This academic debate has simmered for decades but has become critical because computer programs used to formalize or verify proofs require precise and unambiguous definitions, not ones open to interpretation or context that computers lack.

British mathematician Kevin Buzzard of Imperial College London encountered this issue while collaborating with programmers, leading him to reevaluate the definition of ‘equals‘ to challenge common assumptions about equality.

Buzzard’s Revelation on Mathematical Equality

Buzzard reflects in his preprint on the arXiv server that six years ago he believed he understood mathematical equality as a well-defined concept. However, working with computer theorem provers at the master’s level revealed that equality is a more complex and thorny issue than he had realized.

The equals sign (=), created by Welsh mathematician Robert Recorde in 1557 to symbolize equality between objects, was initially slow to gain acceptance. It eventually replaced the Latin term ‘aequalis’ and set the stage for computer science, making its debut in the programming language FORTRAN I exactly 400 years later, in 1957.

The concept of equality dates back to ancient Greece, but modern mathematicians use it somewhat loosely, according to Buzzard.

Traditionally, mathematicians use the equals sign in equations to demonstrate that different mathematical objects share the same value or meaning, a relationship verified through transformations. For instance, the integer 2 can represent a pair of objects, just like 1 + 1 does.

Set Theory’s Influence on Equality

Since the late 19th century, another definition of equality has been in use, originating with set theory. As set theory developed, the notion of equality expanded. For example, mathematicians can consider the set {1, 2, 3} equal to the set {a, b, c} because of canonical isomorphism, which evaluates the structural similarities between groups.

Buzzard explains that mathematicians found it practical to call such sets equal because they align naturally, as he noted to Alex Wilkins of New Scientist.

However, this approach to equality, known as canonical isomorphism, is now causing issues for mathematicians trying to formalize proofs with computers, even affecting foundational concepts established long ago.

“None of the existing computer systems capture how mathematicians like Grothendieck use the equals symbol,” Buzzard told Wilkins, referring to Alexander Grothendieck, a key 20th-century mathematician who used set theory to describe equality.

Some mathematicians propose redefining concepts to formally equate canonical isomorphism with equality.

Buzzard disagrees, urging mathematicians to reevaluate foundational concepts like equality to bridge the gap between their understanding and what computers can process.

“When forced to clearly define what one means without relying on vague terms,” Buzzard writes, “one sometimes has to do additional work or rethink how certain ideas should be presented.”

Read the original article on: Science Alert

Read more: How to Make Math Lectures More Fun