This is not what Gödel says, and in fact your statement is true in a trivial way: you can prove 1+1=2, and Not(Not(1+1=2)), and Not(Not(Not(Not(1+1=2)))), etc. ad infinitum. This is an infinite space of provable true statements that can be exhausted by a ten-line Python script.
IMO, this is why we actually need mathematics -- as a field in which to learn what it means to know what you're talking about.
elendilm · · focus · HN ↗
But Godel's Incompleteness Theorem and Tarski’s Undefinability theorem ensure an infinite space of provable true statements.
Neither LLM's nor humans can exhaust it. So yes, both mathematicians and LLMs are needed.
Both can contribute and there will still be work leftover.
Kotlopou · · focus · HN ↗
IMO, this is why we actually need mathematics -- as a field in which to learn what it means to know what you're talking about.
elendilm_2 · · focus · HN ↗
[dead]