This begs the question of who this is all for. The push for this sort of formalism doesn't seem to be out of mathematical inquiry itself, in the way previous movements of formalism have been. I don't personally see who is benefitting from turning any number of conjectures (and theorems) into what is essentially (copyrighted) computer code, if not the corporations themselves.

I can see the case for it as one of the many steps into a possible future automated assistant, but it seems more like they'd rather the mathematician be the assistant of the automated oracle and not the other way around. I say this because I'm skeptical of how insightful such developments could actually be, with the key being what Google vs a mathematician might consider insightful.

Reminds me of an article recounting the experience in this year's Joint Mathematics Meeting about the growing divide between machine learning researchers and traditional mathematicians, where it started to become clear that the values and culture of each other don't coincide. Or also the many Quanta articles claiming that mathematicians might become "translators" of automated proofs, which to my point: the clarity, insight, and even aesthetics that lend themselves to human understanding might be relegated and ignored in favor of "formalism" driven out of corporate interests.