Skip to main content

- Now I feel as if I should succeed in doing something in mathematics, although I cannot see why it is so very important. (H. Keller)
- Can you "think of" an undefinable number? (R. Israel, comment on stackoverflow)
- I stumbled upon this when trying to understand what one misses when using Henkin instead of standard semantics for higher order logic.

- I simply learn maths by lazy evaluation. (T. Altenkirch, FLoC 2018)
- His answer when I asked whether one needs to be a blessed mathematician in order to understand HoTT.

- A good definition is worth a hundred theorems. (unknown)
- No more "proofs" that look more like LSD trips than coherent chains of logical arguments. (T. Nipkow, G. Klein, preface in Concrete Semantics)
- Great book for a great course that I took at TU Munich - the thing that got me into interactive theorem proving.

- For any (even infinite) collection of pairs of shoes, one can pick out the left shoe from each pair to obtain an appropriate selection; this makes it possible to directly define a choice function, but for an infinite collection of pairs of socks (assumed to have no distinguishing features), such a selection can be obtained only by invoking the axiom of choice. (B. Russell, see https://en.wikipedia.org/wiki/Axiom_of_choice)