> And the study and the creation of those formalisms is not something automatisable.

Lol again. Have you tried it? Go ask your favorite LLM to invent a machine-checkable formalism for something that you vaguely describe to it. It'll oblige. If it's one of the top models and you give it a good budget, it'll do a good job. Very likely it'll do a better job than you.