For the record, Gödel proposition can be constructed[1] in the same manner that Quines[2] can be constructed. I myself have formalized[3] the first incompleteness theorem in the Coq proof assistant, and many others have as well in various proof assistants.
You can find specific and concrete instance of a Gödel proposition written by Stephen Lee at <http://tachyos.org/godel/Godel_statement.html>. It really is not that large of a proposition. I'm not sure how you can claim that proposition that I can see with my own eyes does not exist.
Since you allege the existence of I'mUnprovable propositions renders Peano Arithmetic (see <http://tachyos.org/godel/Godel_statement.html> cited above), Coq, HOL Light, Isabelle and every other proof assistant that has proven the incompleteness theorem inconsistent, I look forward to you facilitating the development of a formal contradiction in any one of these systems. In particular a proof of False in Coq[1] would greatly aid me in getting through some of my troublesome proofs.
Very good. Then surely the paper proof can be translated into an inconsistency of Coq, Isabelle or HOL-light, since all of these proof assistants already prove the existance of such an "I'mUnprovable" proposition.
You can find specific and concrete instance of a Gödel proposition written by Stephen Lee at <http://tachyos.org/godel/Godel_statement.html>. It really is not that large of a proposition. I'm not sure how you can claim that proposition that I can see with my own eyes does not exist.
[1] http://r6.ca/blog/20190223T161625Z.html
[2] https://en.wikipedia.org/wiki/Quine_(computing)
[3] https://github.com/coq-community/goedel