Quotes

  • 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. For an infinite collection of pairs of socks (assumed to have no distinguishing features), there is no obvious way to make a function that selects one sock from each pair, without invoking the axiom of choice.
    (B. Russell, see https://en.wikipedia.org/wiki/Axiom_of_choice)