Here is assumed that if the proof is true and is in a formal language, there is no hidden messages in the text.
That is never something safe to assume. I can write formally correct proofs that contain hidden messages quite easily—add extra lemmas and extra steps. Unless we’re very smart, it would be hard for us to detect which steps are unnecessary and which are needed, especially if it rewrites the main proof thread somewhat.
Another way to check proofs is to run two slightly different non-communicating Oracles and compare outputs.
I’ll accept that as a part of a submission if a) you develop it more, in a formal way, and b) you repost it as a top level comment.
That is never something safe to assume. I can write formally correct proofs that contain hidden messages quite easily—add extra lemmas and extra steps. Unless we’re very smart, it would be hard for us to detect which steps are unnecessary and which are needed, especially if it rewrites the main proof thread somewhat.
I’ll accept that as a part of a submission if a) you develop it more, in a formal way, and b) you repost it as a top level comment.