The Coq mailing list

[Kinan Dak Albab <babman AT bu.edu>]

This has been an interesting discussion to read. I do not have nearly enough depth in fields medal level mathematics or the career and politics of being a mathematician to understand all the subtle implications of having a purely constructive vs classical reasoning framework on that world. However, I want to add something to a previous point, although the discussion seems to have drifted away from it.

I think Ltac deserves more credit than this discussion was giving it. I taught a course last year where we covered using several proof assistants and certified programming languages (from the program verification perspective) to students of various backgrounds, from undergraduate seniors to PhD students. After about 4 weeks of Coq, most students were able to write small but non-trivial tactics for program verification, either to shorten their proofs by repeating some proof pattern directed by the structure of the program being analyzed (e.g. applying case analysis on the condition in an if statement), or for crunching/generating sub-goals with Hoare logic etc.

Most of these students did not have prior background on this kind of formal reasoning or proof engineering, but they were able to use and intuitively understand props and inductive relations in Coq because of their computational content / interpretation. It was considerably more challenging for the students to do something similar in Lean. The theorems and programs they were able to work on were considerably simpler. Part of this may be because I am far more comfortable with Coq, so I may have given better examples or homework exercises. But it was clear that (at least for program verification) tactics are really as important as library theorems and lemmas (if not more so).

I am not entirely sure that providing extensions of any specific system that incorporates different axioms (e.g. LEM) is the way to go. I agree with Talia that having different systems that cater to different communities is perfectly fine, provided that interfacing between such systems is improved. The main shortcoming of the status quo (from my very pragmatic program verification perspective) is the immaturity of programming/proof abstractions for proof engineering, which fail to sufficiently abstract the mathematical foundations of the system, and end up increasing the learning curve and required background for effective use of the system. It is ridiculous to assume that programmers who use strongly typed programming languages need to understand the underlying type theory and logical foundations well, in fact most do not. Unfortunately, this seems to be a requirement for those interested in mechanized proof engineering. Customization is likely to make this worse.

-Kinan

http://cs-people.bu.edu/babman/

On Wed, Jan 8, 2020 at 8:24 PM Conor McBride <conor AT strictlypositive.org> wrote:

Ah, potilics.

-- Sent from my oPhine

> On 9 Jan 2020, at 00:50, Timothy Carstens <intoverflow AT gmail.com> wrote:
>
> https://twitter.com/congressfellows/status/1111721764336422913?s=21
>
> Guilty as charged 😉
>
> Sent from my iPhone
>
>> On Jan 8, 2020, at 4:41 PM, Conor McBride <conor AT strictlypositive.org> wrote:
>>
>> Ah, politics.
>>
>> --not sent from my iPhone
>>
>>> On 8 Jan 2020, at 23:09, Kevin Buzzard <kevin.m.buzzard AT gmail.com> wrote:
>>>
>>>
>>> Since I highlighted Differential Geometry in my previous note, let us look at an example that seems particularly tricky to formalize in our current proof-assistant world: the elliptization conjecture (commonly known as the Poincaré conjecture), which was solved by Perelman in 2003, over a span of three papers (https://arxiv.org/search/?query=grisha+perelman&searchtype=author&abstracts=show&order=-announced_date_first&size=50). Incidentally, Perelman was awarded a Fields Medal for his work.
>>>
>>> Perelman did not accept the Fields Medal (but he was offered it).
>>>
>>> Whilst I have no doubt that LEM and AC will be thoroughly embedded in the Perelman proof, I believe that this has nothing to do with the fact that the proof of the Poincaré conjecture "seems particularly tricky to formalise" (to those not in the area, let me say that this is a *gigantic* understatement). I believe that none of the systems currently even contain a *statement* of the Poincaré conjecture, although Lean is nearly there. I would love to be proved wrong about this (the belief that no system contains a statement! I know full well that no system contains a proof). The reason that none of the systems contain a statement is, I believe, due to the fact that mathematicians are not anywhere near as engaged with these systems as they could be, and hence things like the definition of a smooth manifold have only recently started to appear in these systems (Lean got a definition late last year). The reason that the systems don't contain a proof of Poincaré is that the proof when written out in full is thousands of pages long, no mathematician sees the need to write down a "roadmap" which would be suitable for computer scientists to formalise, and no mathematician sees the need to formalise the proof themselves, because our community has accepted it and hence we see no need to verify it in any formal way. It's just like FLT (which I know for sure uses LEM and AC, at least in all currently known proofs) -- I have said in the past that if you give me $100,000,000 I could hire a team to put in the many hundreds of person-years necessary to formalise the Wiles/Taylor proof (I was a PhD student of Taylor when it all blew up in the 90s and I read the Wiles and Taylor-Wiles proofs carefully) -- but this will never happen because no grant agency would spend that kind of money on a project which most number theorists believe to be utterly pointless (and believe you me, I have asked many number theorists what their opinion on a formalised proof would be). I'm sure that an expert in Ricci Flow could envisage formalising a proof of Poincaré with a similar sum of money. This will clearly never happen and we need another approach. The reason it happened with the odd order theorem was that mathematicians wrote a good roadmap (two essentially self-contained books, by Bender--Glauberman and Peterfalvi) which mathematically-inclined computer scientists could follow, and it probably helped that the odd order theorem was a statement whose proof (not just the statement, but the proof too) mostly involved finite objects and hence LEM/AC were not an issue (some parts of it use representation theory and hence the complex numbers, although the use was not "serious" enough to require non-constructive arguments). Whilst the statement of FLT is elementary, its proof involves many objects from analysis (modular forms, automorphic representations, harmonic analysis, the trace formula) and AC is embedded in the set-up of these theories (as well as in the "patching" argument in the algebra side of things, which relies on Kőnig's Lemma).
>>>
>>> What I believe LEM and AC have to do with this is that I believe that the fact that computer scientists still believe that these facts are still worth talking about puts off the 99% of mathematicians who assume one or both of these facts every day because we mathematicians are told from day one at university that they are both true and that modern "Fields Medal" mathematics is built upon them. The fact that LEM and AC are still some sort of an "issue" in formalisation -- still something worth talking about -- makes the subject feel to the Fields Medal crowd like it is living 100 years in the past; for mathematicians, Hilbert beat Brouwer and that was the end of it. Sure there are some examples of constructivism in modern mathematics. Sure one can talk about doing mathematics in some large class of toposes or whatever, where constructivism becomes an issue. But what I really want to hammer home is that to the "mainstream maths" crowd this whole constructivism thing is weird niche mathematics, uncomfortable as this story sounds to many within the formal proof community. Mathematics undergraduates start using Lean and within an hour will hit some issue about equality not being decidable or trying to get an element from a non-empty type and finding that the `cases` tactic won't eliminate to type -- they ask what is wrong and I tell them to switch on decidability of all propositions and noncomputability of all functions and they'll be fine. Once they do this they can go back to treating mathematics the same way that every single one of their lecturers do. That is what mathematics has become, for better or worse, and the systems that do not embrace this point of view will have a hard time attracting "regular" mathematicians. On the other hand they might perhaps have an easier time attracting constructivists or computer programmers. One has to make choices here. As a "regular" mathematician myself this is why I promote Lean, but if it is true that Coq can also present itself as an environment where "regular" mathematicians can do *all* undergraduate level mathematics without being troubled by foundational issues then I see no reason why Coq cannot attempt to build up a community of "regular" maths users as well. Here's hoping. If any Coq users have mathematician friends who are looking for projects, then *stating* the Poincaré conjecture in Coq (and in particular formalising the definition of a real manifold) would be a great way of showing mathematicians that Coq is capable of talking about modern Fields Medal level mathematics. On the other hand, any talk of proving it in any of the theorem provers is a complete fantasy and will remain so until long after "regular" mathematicians have started to embrace this sort of technology (which still unfortunately shows no sign of happening; most mathematicians still have no understanding of the achievements of Gonthier, for example; they know that the four colour theorem was "proved using a computer" but most seem have no idea of the difference between Gonthier's work and that of Appel and Haken, both of which "used computers"...). I am doing my best to stomp on this ignorance but it is an uphill challenge because the systems still seem to offer very little to the working mathematician (who typically is far less worried about rigour (in the CS/"absolute" sense) than one might imagine; they are far more concerned with having their work accepted by the community, something which is slightly different).
>>>
>>> Kevin
>>>
>>> --
>>>
>>> Coq’s math-comp is an axiom-free formalization.
>>>
>>> R.
>>