• 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)