As an aside, difference between current derivability and final derivability is also an answer to Penrose’s argument about human intelligence being incomputable. Humanity’s mathematical working process can be computable (despite claims based, say, on Gödel’s theorem) because not everything that is accepted as maths is non-contradictory. Sometimes we do need to go back and discard many theorems because the axioms were inconsistent.
As an aside, difference between current derivability and final derivability is also an answer to Penrose’s argument about human intelligence being incomputable. Humanity’s mathematical working process can be computable (despite claims based, say, on Gödel’s theorem) because not everything that is accepted as maths is non-contradictory. Sometimes we do need to go back and discard many theorems because the axioms were inconsistent.