Bartosz Milewski on Nostr: They are arguing that "equals" was a loose badly-defined concept, so they are not so ...

They are arguing that "equals" was a loose badly-defined concept, so they are not so much "redefining" as "defining" it. And the push came from attempts to codify mathematics so it would become acceptable to computers--which are much pickier than human mathematicians.