> The submission process is thorough, but achievable: as a test, I successfully managed to submit my own recent formalization [...] I find this kind of endearing, how he almost makes it sounds like "If even I can do it, you can too!", disregarding he's probably the most prolific mathematician currently alive. Some years ago I suggested it might be interesting to have a kind of blockchain of formally verifiable mathem…
> but was quickly shutdown by people telling me it was a useless endeavor due to Goedels incompleteness theorems
You shouldn't have listened to them, "incompleteness" only applies when you try to encode the language and meta-language in the same encoding—which no one actual does. (For example, programming language syntax is complete.)