Comment by jrflo

Mathematics not being axiomatically complete doesn't mean you can't have crazy progress from a formalized and mechanized systems. It just means that there are corners you can't reach mechanically, but we don't know if those corners are at all interesting or not. It could be the case that 99.99% of useful math can be found mechanically.