[seanhunter]

As far as I can see people always radically exaggerate the effect of the incompleteness theorems. It seems interesting that any nontrivial axiomatic system has statements which are true but unprovable but to say that derails Hilbert’s project seems just obviously untrue when you can for example join math postgrad programs now which are focused on formalisation. [1] So formalisation is very much still going on, probably more so now than ever given advances in theorem provers.

Yes there are undecidable statements (eg the continuum hypothesis) but that doesn’t change the fact that the vast vast majority of statements in any axiomatic system are going to be decidable, and most undecidable statements are going to have “niche” significance like that.

[1] eg https://www.imperial.ac.uk/study/courses/postgraduate-taught...

[random3]

This is more like the popular lay take that are more or less confused about the meaning and implications of the theorems. The fact is that the implications are real yet more nuanced than this - something the article touched on.

Hilbert’s program was to reduce math to a finite set of axioms and was indeed derailed by incompleteness theorems(Gödel) and undecidability (Church, Turing).

Formalizing math with automated theorem provers has little to do with the goal of Hilbert program. Also they aren’t related to the foundational research that it entailed.

Also, as the article mentions, the implications as well as Gödel was largely misunderstood.

[scott_meyer]

Proof by contradiction requires finding a single contradiction. Practical utility just requires that contradiction be infrequent enough.

[pdonis]

> any nontrivial axiomatic system has statements which are true but unprovable

Although this is a common way of stating what Godel's incompleteness theorem tells us, it's actually not correct. As was posted upthread, when you combine Godel's first incompleteness theorem with Godel's completeness theorem (all this in first-order logic), you find that, for any sentence that is not provable in a system of first-order logic (such as the Godel sentence for that system), there must be a semantic model of that first-order logic in which the sentence is false. (I gave an example of such a model for the first-order axioms of arithmetic upthread.)

[dist-epoch]

> As far as I can see people always radically exaggerate the effect of the incompleteness theorems

Like people saying Godel theorems "prove" LLMs could never invent new mathematics because being a software system Godel applies to their operation, but not to humans which are not axiomatic systems, and thus humans can go beyond them and beyond the limits of Godel, humans can "know" a result to be true even if Godel says you can't prove it.

[dehsge]

At the same time if you imagine a machine that can associate different maths. Would said machine encounter undecidable statements more frequently?

Would the rules of said machine have statements they themselves cannot prove by parameters set in their ‘programmed(by humans, machines, or other machines)’ assumptions?

[empath75]

> the vast vast majority of statements in any axiomatic system are going to be decidable

This is just flatly untrue, in the strictest possible sense, and even in the generous definition of "statements that mathematicians care about", that is going to be very heavily biased towards questions that are decidable, because the questions that are likely to be decidable are the ones that they can even reason about to begin with.

If you're a computer programmer, the CS shadow of Godel comes up _all the time_ in practice, and undecidable situations are quite common and don't really need to be carefully constructed.

This is just the drunk-in-the-streetlight situation. Things seem to be decidable everywhere we look because we look where things are likely to be decidable.

[LegionMammal978]

To be fair, in the most literal sense, the vast majority of syntactically-valid statements in a typical FOL encoding will be trivial. One of my side-projects has been trying to find the shortest statements independent of ZF and some of its fragments. In fact, for every slightly nontrivial statement that requires actually building a construction, there are billions more that can be instantly solved via a few simplifications, and statically pruning the search tree a bit is the best we can do.

To actually get independence, we need very rigid statements that don't allow any simple way to fudge a solution or counterexample. If anything, statements that mathematicians (and programmers) care about are biased toward undecidability, simply because they're extremely biased toward nontriviality. We put in the hard work of building towers of rigid definitions to that effect.

[jolt42]

We really want to believe that we can understand everything, yet we know we cannot.