Grothendieck's use of equality

TL;DR

This paper examines how mathematicians, especially Grothendieck, utilize the concept of equality and explores its implications for formalizing mathematical theories.

Contribution

It critically analyzes the role of equality in mathematical practice and challenges common assumptions about its use in formalization.

Findings

Highlights the nuanced use of equality by mathematicians

Identifies potential issues in formalizing equality-based concepts

Provides insights into the philosophical foundations of equality in mathematics

Abstract

We discuss how the concept of equality is used by mathematicians (including Grothendieck), and what effect this has when trying to formalise mathematics. We challenge various reasonable-sounding slogans about equality.