The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

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.