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.

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.

You put it in ~/.TeXmacs/system/bib/, and then type "utcaps" for your bibliography style

Publishing with Mastodon: https://owenlynch.org/posts/2022-04-28-mastodon

- Website
- https://owenlynch.org

I like mixing things, and also general schemes for how to mix things.

Grad student at Universiteit Utrecht.

Enthusiast.

Joined Apr 2022