Comment by JadeNB

Presumably there's not much logical obstruction to all human-understandable math eventually being formalized, although the willingness and ability to commit the requisite enormous amount of time will probably be insurmountable. But definitely that hasn't happened already!