Archive for the ‘reviews’ Category

FOM discussion

October 25, 2014

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



July 30, 2014

Mathgate declares its purpose as a “website for learning logic and mathematics through formal proofs”. The author and owner of Mathgate is Chad E. Brown, who is also the author of Satallax – an automated theorem prover which has won a a couple of times on the CADE ATP Systems Competition. Mathgate is powered by a different prover, however, which is described as follows:



February 1, 2014

ProofPeer is a project to create a cloud-based social network interactive theorem proving system. I wrote about it a year ago. The project looked dormant since about July, but now it got funding and is accepting PhD studentship applications.


Bitcoin epic fails

January 4, 2014

Bitcoin, or more generally cryptocurrencies  is  a somewhat complex subject in that it connects technology, economics and law. But it is kind of fashionable now, so some famous people decide to publicly formulate opinions about it without devoting time and effort to gain knowledge about how the technology actually works. As one commenter on the Marginal Revolution site nicely put it:

The situation has all the makings of your standard paradigm shift, where pundits with less neurological plasticity give future history books lots of look-how-wrong-they-were quotes.
I would like to mention two examples of such epic fails.

The Russell proof language

August 19, 2012

I have thought for a long time that it would be nice to have a high-level proof language with a prover that would compile that to an easy to verify and still readable low level language. A good candidate for the low-level part would be Metamath. I have recently found out about Russel – a high-level proof language created by Dmitri Yurievich Vlasov that compiles to (a simplified version of) Metamath. The Russell project on Sourceforge was last updated in February 2011, so it seems to be unused and abandoned. There is a paper (in Russian) that describes Russell. Unfortunately I don’t have access to the journal where it was published.


The first formalized math wiki is here

April 13, 2011

I have been wondering for a couple of years who will be the first in the race to set up a a publicly available, working and usable formalized math wiki. Now ladies and gentlemen we have the winner and the winner is!


The next generation of proof assistants: ten questions

November 17, 2010

Checking for new stuff on Freek Wiedijk’s home page I stumbled upon slides of his recent talk given at the Workshop on Logical and Semantic Frameworks in Natal, Brasil. He poses there ten questions about how the next generation of proof assistants should look like. In this post I want to give my answers to those questions.

Should the next generation of proof assistants be based on ZFC set theory?


How to Publish Counterexamples in 1 2 3 Easy Steps

May 21, 2010

I found some time to look over recent issues of Notices of AMS and I noticed a letter from Theodore P. Hill, a mathematician from Georgia Tech. The letter led me to read his article “How to Publish Counterexamples in 1 2 3 Easy Steps”. It’s a story that starts when he found errors in a mathematical paper that he got for review and traced those errors to a previously published article in Notices and ends almost two years later in pretty much a complete failure to cause any public admission of the problem and correction from the authors. (more…)

Goodbye ProofGeneral, again

April 4, 2010

A couple of weeks ago Holger Gast announced the first release of the new interactive interface for Isabelle theorem prover. I was planning to write its review, but I decided not to as Jesus Aransay’s wrote a post on the Isabelle mailing list that  pretty much summarizes what would be in that review.

For me the lack of proper display of mathematical symbols and subscripts is a show stopper. You can’t write mathematics without that. I hope that will be resolved soon and I3P will be an excellent replacement for ProofGeneral.

Gödel, Chaitin and formalized mathematics

March 23, 2010

The subject of formalized mathematics has shown up in Slashdot discussions a couple of times. Every time that happened someone mentioned Gödel inconsistence theorems and from that point on much of the discussion concentrated on how Gödel results imply (or not) that formalized mathematics is impossible, impractical or useless.

When I see a discussion like this I think how some seventy years ago a similar forum would discuss the idea that it would be possible and useful to do away with human computers and use machines to execute algorithms. There would be similar arguments about how you could not do that because to execute an algorithm one has to understand it first and machines can not uderstand anything. The art of designing algorithms would lose its beauty when the algorithms would have to be written in a machine language. And, due to a deep theoretical result called the “halting problem” we would have no way to know in advance if such algorithm would ever stop to produce a useful result.

It is easy to dismiss  Slasdot discussions and blame them on the general cluessness of the Slashdot crowd. However, I recently stumbled upon the text of a talk given by Chaitin at the University of Cordoba in November last year that completely puzzled me. (more…)