The modern computerized-proof world is such a delicious mashup of the arch-rivals Hilbert and Poincare.

Hilbert had a grand dream that when two people disagreed, they could just say "calculamebus" (let us calculate), yet this was married to the "analytic" viewpoint of set theory. Poincare had a disdain for logic, and yet still championed a "synthetic" viewpoint that was key for the development of constructive mathematics!

The modern proof assistant owes a debt to both.

Erratum: looking at my source (logicomix), Hilbert said "In mathemathics, there is no ignorabimus", meaning there is no "we shall not know". Leibniz says calculemus.

Sign in to participate in the conversation
Mathstodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!