Did Gödel prove that some truths can never be proven?

Not quite. What Kurt Gödel proved in 1931 is narrower, and in some ways stranger: any consistent set of rules for doing arithmetic, of the kind a computer could check, leaves some true statements about numbers that those rules can't prove. A second theorem adds that such a system can never prove its own consistency. So it's not that some truths are unprovable by any method at all; it's that no single fixed rulebook can capture all of arithmetic.

His trick was to make mathematics talk about itself. Gödel gave every formula a number, so statements about proofs became statements about numbers. Then he built a sentence that, in effect, says "I am not provable in this system". If the system is consistent, it can't prove that sentence, which means the sentence is true. You might think you could just add it as a new rule. You can, but the bigger system then has its own unprovable sentence, and so on forever.

The timing was dramatic. At a 1930 conference in Königsberg, the great mathematician David Hilbert gave a farewell speech arguing that every mathematical problem can be solved, ending with "We must know. We will know!" At the same meeting the young Gödel announced his first theorem. Almost nobody noticed, except the brilliant John von Neumann.

What it doesn't mean matters just as much. It doesn't say mathematics is broken, and it doesn't apply to weaker systems: arithmetic with addition but no multiplication is complete. Uses of Gödel outside logic, from sociology to claims about the human mind, have been sharply criticised.