Follow

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.

@olynch calculēmus?

calx: a pebble

calculus: a tiny pebble

calculāre: to calculate

calculāmus: we calculate

calculābimus: we will calculate

calculēmus: let us calculate

calculētur: let it be calculated

calculandum est: it ought to be calculated

...

As far as I know, "calculāre" is a modern coining. The Romans would have said "calculōs subdūcere": to take away pebbles (i.e. counters), to mean "to calculate".

Owen Lynch@olynch@mathstodon.xyzErratum: looking at my source (logicomix), Hilbert said "In mathemathics, there is no ignorabimus", meaning there is no "we shall not know". Leibniz says calculemus.