Comment by hypersoar

The incompleteness theorem says that there are statements which can be neither proven true nor false in a given axiomatic system. If there is a proof to write in lean, then the statement is already outside the bounds of incompleteness.