The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Kevin is deeper into the math world than I, but this matches my experience on all points.

"Name brand" mathematicians, just like physicists, computer scientists, and software engineers, only care about one thing: doing work which makes sense for their careers.

Strategic realism dictates that, if I saw a path towards proving the Jacobi conjecture, I would not bog myself down with constructive concerns unless I absolutely had to. Why would I? Even a proof-sketch would be enough to advance my career (perhaps even more-so than a completely worked proof!) Professional mathematics is a fundamentally social activity and "finished proofs" are more like milestones than atomic units of work.

There is an entrepreneurial angle to this thread that I think could be profitably recognized.

Suppose I'm in the business of building tools for metal working and machining. How can I win new customers? One method is to make incremental improvements to the state of the art: "This is a drill press. You already have a drill press, but this one offers better value over its lifetime. Your employees already know how to use a drill press, so it won't be much work to train them on how to use this new one."

Another method is to make changes to /the broader work process./ "This is a Foo and this is a Bar. They seem funky, but together, they replace your drill press, chop saw, and micrometer. Your employees have no clue how to use these things, your designers don't know how to design for them, and your project managers don't know how to plan timelines around them. But once they're trained, they'll be more efficient than people who are still using outdated drill/chop/meter tech."

Back to math, CS, and mechanized logic. Sometimes these discussions feel like an attempt to squeeze these new ideas into the 1st kind of pitch. "Dear mathematicians: your life will be the same as it is now, except that faulty proofs will be less common. The only price is, you need to revisit your notions of LEM and AC." I dunno man, hard sell.

If you want to pitch a new foundations [and as far as I can tell, *all* mechanized foundations are a "new foundations" relative to ZFC+pdf], I think you need to offer a bigger impact. What other parts of the mathematician's dayjob/ecosystem will be impacted?

I think we could learn a lot by talking to math grad students about these matters. When I was a grad student, I would have *loved* to live in a world where PDFs had hyperlinks to the relevant definitions. For example, a formal wikipedia+mathoverflow+arxiv mashup of some kind would have completely changed the grad student experience for me.

As to particulars of which logic with what properties, I suspect that different trades will continue to work in environments that are productive for their purposes.

It's almost as if we need a system which lets us define, study, and relate "domain specific logics," some kind of foundation beneath the foundation, some sort of ... meta-math perhaps ? :)

-t

On Wed, Jan 8, 2020 at 3:09 PM 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.