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