## FOM discussion

I am not really convinced by the discussion on FOM that HoTT is “better” than ZFC in any universal sense. To me it looks rather that HoTT approaches the body of mathematics from a different side, figuratively speaking. This puts certain areas with active research (some subjects in algebraic topology) closer to foundations and therefore makes them easier to formalize, but at the cost other areas being put farther away. It is not obvious that this trade off is worth abandoning the whole traditional style of doing (even informal) mathematics which is very set theory oriented.

There have been some quite amusing moments in the discussion. One participant, rather sceptical to formalized mathematics posed the following question:

Here is a very simple statement which I often give to students as a first exercise in iteration, and to practice formal mathematics.

***
Let f be a real-valued function on the real line, such that f(x)>x for all x.
Let x_0 be a real number, and define the sequence (x_n) recursively by x_{n+1} := f(x_n). Then x_n diverges to infinity.
***

(…)
What effort would be required to formalize this kind of statement using current technology?

The funny thing here is that the statement is false. To see this, just take any sequence $x:\mathbb{N}\rightarrow\mathbb{R}$ that is increasing and bounded and for any $y\in \mathbb{R}$ define $f(y) = x_{x^-1(y)+1}$ if $y\in x(\mathbb{N})$ and, say $f(y) = y+1$ otherwise. Then we have $x_{n+1} = f(x_n)$ and $f(y)>y$ for all $y\in\mathbb{R}$, but we have chosen the sequence $x$ to be bounded…

This was used by some to point out usefulness of checking proofs by a machine, which would catch a mistake like this. Freek Wiedijk was polite enough to add the missing assumption about continuity of $f$ and provided a HOL Light verification script for a similar (but true) theorem. That didn’t work too well: Harvey Frieman called that script a “totally unacceptable ugly piece of disgusting garbage”. I think that was a bit too harsh – the second version written using Freek’s declarative miz3 language for HOL Light didn’t look that bad.

Isabelle/ZF on which IsarMathLib is based was mentioned in the discussion once – but only to say that it “hardly has any users”. Well, that was better than calling me “nobody” (as in “nobody uses it”) that I have seen before.