Why Mathematicians Still Struggle to Define Equality in the Computer Age

The article unpacks why the everyday mathematical idea of equality is far more subtle than it appears, showing how attempts to formalize it in theorem provers like Lean reveal gaps between mathematical intuition, set-theoretic definitions, and type-theoretic frameworks — and why building better digital mathematical libraries may eventually bridge these worlds.