There is a very interesting discussion about formalized mathematics going on the Foundations of Mathematics mailing list. The most interesting part of it (at least to me) is the thread about relative merits of Homotopy Type Theory (HoTT) and set theory (ZFC) as foundations for formalized mathematics. I should probably write what is Homotopy Type Theory here, but since I know very little about it this is too much risk to say something stupid, so I suggest that interested readers have a look at the above link, or read at least the abstract of the recent article about this in the Bulletin of the American Mathematical Society. Replacing ZFC with HoTT as standard foundation for mathematics is an idea of Vladimir Voevodsky – a Fields Medalist from 2002. The main argument for the idea is that it is easier to create research level formalized mathematics (in a proof assistant) when the foundation is HoTT than when foundation is set theory. So the story is interesting from this perspective – that a prominent mathematician is using a proof assistant (COQ) for research and that ease of formalization is an argument for some mathematical idea – for the first time, to my knowledge.
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 
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 
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.
we can define a collection of singleton sets with elements from the set 
. Sometimes vertical bar is used instead of the colon, and in Isabelle/ZF a single dot is used (something like 
parses successfully in Isabelle/ZF). In some programming languages a similar notation is used for lists. For example in Python one can write
