alt Hacker News(Sighs)
Goedel's theorems don't stop AI from finding and formalizing math results. They certainly don't stop AI from making conjectures or writing definitions. They have nothing to do with any of that.
The theorems are about inability of formal theories to prove certain sentences involving provability (the first is about "this sentence is not provable", the second is about "this theory is consistent"). Most mathematicians never touch any such sentences in their entire career. All the life's work of someone like Gauss, an all-time great, can be formalized just fine.
I'm not surprised your understanding of Gödel's findings and their implications is just as superficial as that of maths and philosophy of mathematics in general. Gödel's work has implications way beyond self-referential logic games, and cannot be swept in a corner where it can be safely ignored. For example, there are certain diophantine equations that have no general solution due to Gödel. Also, worth discussing are the Continuum Hypothesis, Whitehead's Problem and stuff like Paris–Harrington Theorem, Goodstein’s Theorem, etc. Not to mention the huge impact on computer science with the Halting Problem, Rice's Theorem and others. In fact Gödel's work actually spawned CS as a field of study.
The idea that maths is just the study of arbitrarily thought-up formal systems is just a very naive idea that doesn't actually reflect reality, once investigated in depth. Anyway, I have feeling you will let nothing rob you of that sweet feeling of having "magical predictive capacities", so I'll be on my way. I've already dropped some bread crumbs if you're interested in actually expanding your horizons and getting in the weeds, where things are not as straightforward anymore. But beware, "here there be monsters". Godspeed!