He is refering to the late 19th and early 20th century work on the foundations of mathematics amoung mathematicans and philosophers. They attempted to fully formalise mathematics. Serveral approaches and schools in mathematics all hit various paradoxes, often of the same kind, and this ultimately culminated in Godel's incompleteness theorems:

https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

https://plato.stanford.edu/entries/goedel-incompleteness

There's also a thing called "the halting problem" which is related to this. Because without the halting problem you could solve any mathematical proof by simply turning it into a computer program that brute forces the problem domain and calculating whether the the program will terminate or not. Of course, this is impossible.

That's a bit backwards. The halting problem is a computer-flavored variant of Gödel's work. A very simple part -- it's essentially a computer program that says "The program that produced this string is lying".