[FOM] Crisis Management and Mitigation in Foundations of Mathematics

[José Manuel Rodríguez Caballero]

Dear Patrik,

Voevodsky was interested in the accumulation of mistakes in papers. In this
lecture he explains the situation in his own research area and how he tried
to solve this crisis using a proof assistant based on HoTT (it could be
Lean, Coq or even Isabelle/HoTT):
https://www.youtube.com/watch?v=E9RiR9AcXeE

According to my experience, simple type theory (Isabelle/HOL) is more
practical in order to formalize traditional mathematics:
https://arxiv.org/abs/1804.07860

Coq and Isabelle/CTT are good for formalizing constructive mathematics:
https://isabelle.in.tum.de/website-Isabelle2016-1/dist/library/CTT/CTT/document.pdf

The team of Isabelle/HOL is finding mistakes and gaps in publications. For
example, Manuel Eberl https://www21.in.tum.de/~eberlm/
sent me the following mistakes and gap that he found (this is only one
person, imagine the global picture of mathematics!):

"Off the top of my head, I can also think of a few more things:"

– When I formalised the Ilie–Navarro–Yu algorithm [4], I found that they
assume the transition relation of the input automaton to be total, which
they never mention anywhere in the paper.

– In one version of their paper, Bhat et al. used an unsound rule in the
probability density compiler. I found that while formalising it. [5, 6]

– Leighton's widely cited proof of the Akra–Bazzi theorem omits a case
distinction. It is fixed relatively easily once you know how to, but I was
stumped for a while [7,8].


[1]: http://www21.in.tum.de/~eberlm/sds.pdf
[2]: https://dl.acm.org/citation.cfm?doid=3184466.3125642
[3]: http://dss.in.tum.de/files/brandt-research/sds2smt_journal.pdf
[4]: https://www21.in.tum.de/~eberlm/nfasim.pdf
[5]: https://link.springer.com/chapter/10.1007%2F978-3-662-46669-8_4
[6]: https://www21.in.tum.de/~eberlm/pdfcompiler_esop.pdf
[7]: https://link.springer.com/article/10.1007/s10817-016-9378-0
[8]: https://www21.in.tum.de/~eberlm/divide_and_conquer_isabelle.pdf
[9]: https://hal.inria.fr/hal-01289616v1/document

The only hope that I see for the mathematical tower do not fall with the
exponential explosion of knowledge is to supports projects like ALEXANDRIA:
https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/

There are many myths against proof assistants. So, I would be important to
have workshops in which professional mathematicians could interact with
experts and users of proof assistants, in order to gain confidence in this
new technology.

Sincerely yours,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190309/69fed467/attachment-0001.html>