- Now I feel as if I should succeed in doing something in mathematics, although I cannot see why it is so very important.
- 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.
- 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)