Read on Twitter
Isabelle/HOL has schemes! https://www.isa-afp.org/entries/Grothendieck_Schemes.html . The formalisation is due to Bordg, Paulson and Li. In this thread I will try to explain why this is a big deal. 1/n
The HOL in Isabelle/HOL stands for "higher order logic". Despite sounding quite fancy, this logic is actually in some sense weaker than another foundational logical system called "dependent type theory", used by Lean and Coq. Why should a mathematician care about this? 2/n
Mathematicians typically do not really think about what foundations they're using -- indeed mathematics worked fine for millennia without any foundations at all! (think Gauss, Euler). But actually Gauss and Euler were using a limited set of tools. What do I mean? 3/n
Gauss and Euler could happily consider subsets of things which already "existed", like Z[sqrt(2)] and so on (subsets of the reals), but they never made that abstract leap to "a ring is an abstract set + some structure + some axioms". This didn't happen until later. 4/n
People doing abstract commutative algebra like Emmy Noether were happy to work with this extra abstraction -- this abstract concept of a "set" which didn't have to be a subset of something that was already in the mathematical canon. 5/n
And then along came sheaf theory. This was yet another layer of abstraction. A sheaf of abelian groups on a topological space is a...function? From the set of open subsets of the space to the...set...of...all abelian groups? Wait a minute. 6/n
A category theorist would tell you that a sheaf of abelian groups is not a function, but a functor, with target a large category. ZFC was designed decades before this sort of thing became a thing, and was not designed to deal with such exotic "functions". 7/n
OK so now you have two choices. You can start jumping through hoops and squeezing algebraic geometry so that it fits into ZFC. This can be done! Here's Johan de Jong doing it in the Stacks Project: https://stacks.math.columbia.edu/tag/000H 8/n
The thing is -- everyone knows that this part of Stacks is "weird". It is not *actually* about algebraic geometry at all. It is about forcing algebraic geometry into a foundational system which was not designed to cope with it. Nobody actually *reads* this stuff. 9/n
Grothendieck did not believe in wasting his time doing this kind of exercise. In SGA4 when the going got tough he explicitly left ZFC and added an extra axiom -- the universe axiom -- to his mathematics, so he could do more algebraic geometry. 10/n
Grothendieck's axiom of universes was not a theorem of ZFC. In fact, even less was true! His axiom implied that ZFC was consistent, so by Goedel his axiom was strictly stronger than ZFC. He had broken free! Five years later his ideas had proven the Weil conjectures. Oops. 11/n
What was a set theorist to think? The Weil conjectures are basic questions about the number of solutions to polynomial equations mod p, and the statements could certainly be formalised in ZFC set theory. But the proofs used this weird extra axiom! Was this allowed? 12/n
"Don't panic", said Deligne: "I can do all of this stuff without assuming the extra axiom". Deligne wrote SGA4.5, where all the main ideas for the proof were established in good old ZFC. Apparently Grothendieck disapproved. Now let's fast forward to Lurie and Scholze. 13/n
These stories show that *when it comes to algebraic geometry*, ZFC begins to creak at the seams. The last time I am aware that Scholze made a concrete effort to put his recent mathematics into ZFC is section 4 of https://arxiv.org/abs/1709.07343 where again he squeezes stuff into ZFC 14/n
Since then, my impression is that he is tiring of this. This condensed set stuff (his work with Clausen), and the parallel work of Barwick-Haine, just basically assume Grothendieck's axiom and press on. Similarly Lurie's recent work also assumes universes. Details? Sure: 15/n
Here are Scholze and Lurie discussing these issues: https://mathoverflow.net/questions/382270/reflection-principle-vs-universes . OK, let's get back to schemes, and why Isabelle/HOL's formalisation is a big deal. 16/n
Looking again at that MO post, here I guess people are arguing that everything could *in theory* be squeezed into ZFC. But the more complicated life gets, the more technical and tedious this whole business becomes. Do we want great mathematicians wasting their time on this? 17/n
Lean's type theory, and Coq's, have (a type theory version of) Grothendieck's axiom. I formalised the definition of a scheme with two undergraduate students, and none of us knew a thing about reflection principles and universes -- we just wrote down the defn in the books. 18/n
Isabelle/HOL uses a weaker system, and for them the fact that a sheaf isn't actually a function, or at least isn't naturally a function (because the target "set" is too big to be a set) is a genuine obstacle. 19/n
Isabelle/HOL is an amazing system for doing certain kinds of mathematics. Avigad formalised the prime number theorem, Eberl an absolute ton of 20th century analytic number theory, and a bunch of other analysis has been done. No need for universe axioms here though. 20/n
Last year I challenged the Isabelle/HOL community to do some algebraic geometry in their system: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ . I didn't even know if anyone was listening. Turns out Bordg was. 21/n
Using something called locales, Bordg, Paulson and Li have managed to define schemes and prove the "test case" theorem -- an affine scheme is a scheme! In particular they have shoehorned Grothendieck's definition into a logic system which wasn't designed to handle it. 22/n
I had "written off" Isabelle/HOL as being too foundationally weak to do 21st century algebraic geometry and I now need to re-evaluate my position. Congratulations to all concerned. 23/23, n=23.
PS Isabelle might be able to do Grothendieck but right now we're proving that Lean can do Clausen-Scholze ;-) https://github.com/leanprover-community/lean-liquid/ . Check out Commelin/Massot's beautiful blueprint: https://leanprover-community.github.io/liquid/
