[FOM] Kenzo software finds error in published homotopy theorem
Timothy Y. Chow
tchow at alum.mit.edu
Mon Nov 3 10:59:45 EST 2014
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,
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?
More information about the FOM