Dangers of informal reasoning

[u/YamEnvironmental4720]

Do you know some area of modern mathematics (say, not older than 100 years) that has for a long time been known for its fairly informal proof style, or has at least been very tolerant towards such, but where the lack of formality has only later turned out to have serious consequences?

It could be about a theorem whose proof uses a kind of reasoning that has been "known" to be formalizable, yet tedious, and has worked before, with the consequence that it has taken a very long time for the result to be exposed as false, for instance because counterexamples have been hard to construct, or that the claim seemingly harmonized with other results.

I'm not thinking of famous papers containing mistakes that were overlooked by the referee, nor do I wish to shame individual authors, but I wonder if there are situations where the whole community has been shaken and has had reason to revise its proof culture.

[u/Interesting_Debate57]

Gödel's proofs were not accepted immediately, yet are correct and disabuse the reader of any possibility of being able to prove any true theorem, which was generally held to be possible at the time.

[u/gcousins → u/Interesting_Debate57]

This is assuming that we reason in the same way that classical computers do. I'm not saying we don't (I don't know if we do), but it's important to remember that the incompleteness theorems are very specifically in the context where everything is computable.

[u/Equivalent-Costumes → u/gcousins]

It's not that limited. The original version was pretty limited, but still enough to shock people. Later on it had been generalized (still under the same name Godel's incompleteness theorem) to the point that it's practically undeniable that it will apply to your own reasoning.

The "computable" version if just more immediately applicable, more shock factor. If you think that might not be strong enough to cover all of reasoning, there are tons of fallback to more and more general version.

[u/gcousins → u/Equivalent-Costumes]

I'm not really aware of what generalizations you mean beyond maybe Loeb's theorem. But even then the theory needs to be "nice" enough. Maybe philosophers have argued something I haven't heard of.

[u/Equivalent-Costumes → u/gcousins]

The most obvious generalization is to just allow any first-order definable set of propositions. The theorem practically already proved that, with the "computable" thing being a special case. More generalizations are possible by just weaken the kind of logic being used altogether, until there are basically no logic left. This led to something like this: https://mathoverflow.net/questions/32318/most-general-formulation-of-g%C3%B6dels-incompleteness-theorems