Hilbert Brouwer math feud and the rise of AI proofs — SkimNews
Get the Health newsletter
Daily health & science — research, biotech, public health, the studies worth knowing. Free.
- David Hilbert proved in 1888 that a finite generating set of invariants exists for a large class of algebraic objects without specifying what the set contains, using proof by contradiction and the law of the excluded middle.
- Paul Gordan, who had spent his career on the same problem, dismissed Hilbert's proof as 'not mathematics, that is theology,' though he later conceded 'theology does have its advantages.'
- L.E.J. Brouwer rejected Hilbert's formalism through intuitionism, arguing non-constructive proofs were 'cheating' and that mathematical objects must be mentally constructible; he objected specifically to applying the law of the excluded middle to infinite sets.
- Hilbert retaliated against Brouwer in 1928 by firing the entire editorial board of Mathematische Annalen to remove him, prompting co-editor Albert Einstein to resign and call the dispute a 'frog and mouse battle among the mathematicians.'
- Kurt Gödel's incompleteness theorem later showed the symbol-manipulation game Hilbert championed could never be fully consistent, though Gödel drew inspiration from Brouwer in his own fight against Hilbert.
- The ideas now inform computer science via Alan Turing's work on computability and are resurfacing as mathematicians turn to AI and formal proof verification, with the author suggesting Brouwer may get the last laugh if AI produces verified non-constructive proofs humans cannot understand.
Why it matters: The Hilbert–Brouwer dispute, once dismissed as ivory-tower philosophy, now has practical stakes: as mathematicians increasingly rely on AI-driven formal proof verification, the field faces a near-term scenario where machine-readable proofs are certified as logically true but exceed human comprehension — vindicating Brouwer's intuitionist insistence that mathematics must be constructible to be meaningful.
Ask SkimNews
