Carlos Simpson and VHS

Stream: maths

[Kevin Buzzard]

Carlos Simpson (a mathematician) wrote this article [NB: now links to ArXiv] on computer theorem proving in 2003. I'd not seen it until today. At the end of it he talks about formalising a proof that some space coming up in the study of variation of Hodge structures is negatively curved. If this sounds like a big deal today (and it does, to me) then perhaps it sounded like a massive deal in 2003.

In the last couple of pages of the paper, Simpson writes down a sketch of how he imagines this theorem should be proved in a computer proof checker. I don't want to quote it all here, it's about three pages long. But it might be interesting to know how far we have gone down this route and how feasible people think this plan is to pull off in Lean.

[Kevin Buzzard]

I particularly like that he refers to what I call mathematics as "standard mathematics" and all the constructive stuff as "exotic mathematics" :D

[Johan Commelin]

Incidentally, this is the same Simpson that found a mistake in Voevodsky's papers, and drove Voevodsky towards formalisation.

[Bryan Gin-ge Chen]

Here are a few more related articles by Simpson on the arxiv:

• "Set-theoretical mathematics in Coq" (which appears to be a revision of part of the article Kevin linked above),
• "Formalized proof, computation, and the construction problem in algebraic geometry", and
• "Explaining Gabriel-Zisman localization to the computer" (see also "Files for Gabriel-Zisman localization").

[Johan Commelin]

If the makers of other systems feel impelled at this point to say “hey, our system does just as well or better”, the main point I am trying to make is: That’s great! Try to get us working on it!

[Johan Commelin]

Once we have a reasonable control over the basic notions of ring, algebra, module etc. then much of commutative algebra can be done without any new notational worries.

And here we are... moaning about commutative diagrams and problems with really getting comm.alg. goin.

[Kevin Buzzard]

Do they have these problems in Coq? That was the system Carlos had experience in.

Of course the moans are only that stuff is annoyingly fiddly, not that it is impossible...

[Johan Commelin]

Well... how much commutative algebra has been added to the system after the great module refactor?

[Jesse Michael Han]

But it might be interesting to know how far we have gone down this route and how feasible people think this plan is to pull off in Lean.

I think we're about halfway through the sketch and in the middle of the paragraph about sheaves

[Kevin Buzzard]

My link above now points to the 2004 version of the article on ArXiv. It seems to me that we are basically on the last page of the article (p25), modulo para on p24 which mentions the construction going from schemes over C (which we have) to complex manifolds (which we have).

I think that it is interesting to note that whilst this article was written by a mathematician in 2003, the vision he spells out involves formalising precisely the things (manifolds, schemes, topological groups, sheaves) which mathematicians in 2018-20 were pushing to get, completely independently.

[Kevin Buzzard]

Johan Commelin said:

Well... how much commutative algebra has been added to the system after the great module refactor?

Things like Hilbert Basis? And I'm in the middle of Nullstellensatz? Of course Kenny's absence this year has slowed things down but on the other hand analysis is now moving much faster.