mio (@mio)

Claim. Formalization is an inherently informal activity.

Suppose you have done A informally on paper, and hopefully rigorously too, where A stands for Amazing Theorem.

Suppose further that you published A, after the reviewer(s) and the editor were satisfied with the rigour and the level of amazement.

Then you decide to formalize it, for whatever reason.

You do it, I claim informally, by sitting in front of a computer and typing things, which the proof assistant accepts and rejects successively in an interactive way, as so-called proof assistants work.

Or you give it for an LLM to do it faster while you drink coffee. It doesn't matter. My conclusion will be the same.

All the computer will check is what you typed in the keyboard.

It has no way of knowing whether you or the LLM actually formalized A or something else.

You have to check it yourself (the LLM can't), and the checking is inherently informal, because one of the things the checking involves is the informal input itself.

And of course the checking has to be rigorous, too.