[FOM] Kenzo software finds error in published homotopy theorem

[Timothy Y. Chow]

Let me first thank those who have contributed to the HoTT discussion. 
Although some people have quit the FOM list in disgust, I have found the 
discussion quite illuminating and have a much better sense now for what 
HoTT does and does not offer.

On a not entirely different note, I just read an interesting article in 
the Nov 2014 issue of the Notices of the AMS by Duran, Perez, and Varona: 
"The Misfortunes of a Trio of Mathematicians Using Computer Algebra 
Systems: Can We Trust in Them?"  They describe a bug in Mathematica 
involving exact integer arithmetic (!) that seems to have been introduced 
between versions 7 and 8 and was still present as of the writing of their 
article.  More interesting, perhaps, for FOM readers is that at the end of 
their article, they mention in passing "the recent success of the 
mathematical software Kenzo in detecting an error in a published 
mathematical theorem."  They refer to

A. Romero and J. Rubio, Homotopy groups of suspended classifying spaces: 
An experimental approach, Math. Comp. 82 (2013), 2237-2244.

This paper is easy to find online.  I learned that Kenzo is a specialized 
computer algebra package for calculating homology groups and (in some 
special cases) homotopy groups.  In the course of their computational 
experiments, they detected a discrepancy with a theorem published in 2010 
(by some other authors).  Examination of the proof of the theorem 
uncovered a mistake.

This is still not quite an example of what someone on FOM recently asked 
for because Romero and Rubio were not attempting to formalize the theorems 
in the other paper.  Moreover, Kenzo is a "traditional" computer program 
and not built on top of a proof assistant.  However, the authors are aware 
of the issue of the correctness of Kenzo, and Rubio has co-authored other 
papers that formalize some theorems in homology in Isabelle and Coq:

J. Aransay, C. Ballarin, and J. Rubio, A mechanized proof of the basic 
perturbation lemma, Journal of Automated Reasoning 40 (2008), no. 4, 
271-292.

C. Dominguez and J. Rubio, Effective homology of bicomplexes, formalized 
in Coq, Theoretical Computer Science 412 (2011), no. 11, 962-970.

A natural question arises: Does HoTT offer advantages over Coq/Isabelle in 
the formalization of the above theorems?

What about Kenzo?  Rewriting it so that its results are formally correct 
must incur a computational cost.  Is it possible to estimate how much of a 
slowdown that would be?

Tim