I like Wolfram and always enjoy reading his posts. An irreconcilable thing here is Wolfram clearly wants the Mathematica language to be central to the development of math as a field, but it's proprietary and so there is no guarantee it will survive the dissolution of the company if/when that happens. With Lean & others you can fairly safely assume that a particular version will be archived somewhere, and so a proof formalized for that version can be checked at any time. Not so with Mathematica. It's unfortunate, Mathematica is a cool language, but that's just the structure of incentives at this time. This is without getting into what a proof formalized in Mathematica would even mean, the relative maturity of the kernel and the possibility of there being multiple kernel implementations for cross-checking, and so on.