The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

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.