The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

LEM seems to be a big point of contention. In several mathematical fields, one would like to work without LEM. To quote Bell’s notes on (basic) differential geometry [http://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf], “We observe that the postulates of smooth infinitesimal analysis are incompatible with the law of excluded middle of classical logic“. In modern algebraic geometry too, I find no reason to do classical reasoning. And of course, current research in model theory has little regard for classical reasoning.

The larger point to be made here is that a proof assistant should aim to embed _all_ of mathematics, as opposed to, say, providing conveniences for embedding a lot of advanced-undergraduate level mathematics at the cost of being able to do larger things.

There seems to be some excitement about formalizing “Fields medal level” mathematics, but I think this excitement is entirely unfounded. The mathematical community is just starting to understand Lurie’s 2019 work [https://www.math.ias.edu/~lurie/papers/Conceptual.pdf], let alone being able to formalize it in any proof assistant. But let’s not get too excited about recent work; indeed, even Hironaka’s seminal desingularization theorem from 1963 [https://www.jstor.org/stable/1970486?seq=1#metadata_info_tab_contents] was only fully understood by the mathematical community in the early 2000’s. Even the simplified proof [https://arxiv.org/pdf/math/0401401.pdf] is much too complicated to even understand.

To build solid foundations for a proof assistant, one must, at least on pen-and-paper, be able to embed mathematical structures in suitable (∞, 1)-topoi. Indeed, Shulman’s work from 2019 builds a Quillen model category for interpreting HoTT [https://arxiv.org/pdf/1904.07004.pdf]: this line of work holds much promise, in my opinion. From the little that I understand, ∞-categories have some limitations, and mathematicians are just starting to play with ω-categories, but I can’t say much more about this.

--

I could find no literature on Lean’s VM, and there is very little literature on Lean in general. This is a bad sign.

R.