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.

· · Web · 2 · 1 · 2

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.

@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".

@antiselfdual Oh yeah, thank you! Calculēmus for sure. I don't think that Hilbert was trying to speak like a roman, he just spoke in latin because that's what one did back then.

Sign in to participate in the conversation

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