That's not right! Gödel proved that PM couldn't do what people like Hilbert (or PM's authors) hoped it could do. However, we still have * mathematics * forma

That's not right! Gödel proved that PM couldn't do what people like Hilbert (or PM's authors) hoped it could do. However, we still have * mathematics * formalized mathematics * mathematical research despite the incompleteness phenomenon. All of them are still making progress, even often using approaches that are no more powerful than PM's approach. There are still interesting and important conjectures that can be resolved by a PM-like system, but haven't been resolved yet. I'm sure lots of mathematicians were deeply disappointed when they understood Gödel's result, but it didn't persuade anyone that mathematics was over or that we should no longer work within formal systems!