Grothendieck, Equality, and the Trouble with Formalising Mathematical Arguments

The article examines how mathematicians freely identify objects “up to unique isomorphism,” why this practice collapses in formal theorem provers, and how modern proof systems like Lean force a more precise treatment of equality that exposes gaps—and generates new mathematical ideas.