The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

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.
>>