is dependent type theory a must to define a sheaf?

Stream: maths

[Bulhwi Cha]

Kevin Buzzard said:

I'm using dependent type theory because the concept of a sheaf is a central idea in modern algebraic geometry (which is essential for the proof of FLT) and a sheaf is a dependent type.

I don't know anything about algebraic geometry, but I've seen an article that presented a formalization of sheaves of rings and schemes in Isabelle/HOL and proved that an affine scheme is a scheme: https://doi.org/10.1080/10586458.2022.2062073.

[Kevin Buzzard]

Yes that's correct, but unfortunately the sheaf of rings is not rings in the typeclass sense, it's rings in the locale sense (so all of the theory of rings developed using typeclasses in AFP cannot be applied to the definition). This paper was Paulson's response to my challenge to do any algebraic geometry in Isabelle, and he succeeded. I didn't want to continue the argument because it would look like sour grapes -- he proved it could be done. But here is a question I wouldn't have a clue how to do in Isabelle: "Define categories and functors. Define the concept of an adjoint functor. Now prove that the Spec construction (making a scheme from a commutative ring) and the "global sections" functor (making a commutative ring from a scheme) are adjoint functors". My understanding is that there are currently 4 definitions of a category in AFP and I am not clear about whether any of them would be suitable for stating this question (and the first challenge would be to state the theorem; this is a much more reasonable challenge than actually proving the theorem). I would be interested to hear the opinions of Isabelle experts on how one might go about such a challenge.

But for me the important question is not "is it technically possible to somehow do this" (and it could well be if you jump through some more hoops), it is "could you actually imagine developing algebraic geometry like this?" It's hard enough doing it in Lean when you have more appropriate tools available. Larry's work stimulated no further developments in algebraic geometry and it might be the case that the definition is mathematically correct but unusable in practice; I don't know enough about Isabelle to know the situation here. In Lean we have proved our definition is usable.

[Jireh Loreaux]

Kevin Buzzard said:

But for me the important question is not "is it technically possible to somehow do this"

Right, it's obviously technically possible, because they have (almost) the same proving strength (modulo adding some inaccessible cardinal axioms to Isabelle).

[Utensil Song]

While it might not directly answer the question whether it's a "must", my takeaway of Schemes in Lean is that a dependent type theory based ITP forces specifying things and proof steps explicitly, which leads to more general definitions and proofs, as specialized arguments in informal proofs would be no longer convenient in such an ITP, but the more general approaches have become more natural.

It takes much longer and iterations of design choices to reach this state, but ultimately the result would be an advance of math itself. Dependent type theory based ITP has given the drive for people to fight the overlooked details, refactor the formalism, and achieve a deeper understanding of the subject.

[Chelsea Edmonds]

I wasn't a part of this particular project in Isabelle, (and sadly don't really have the mathematical knowledge necessary to try the definition suggested by Kevin ... at least quickly!), so others may be better to comment here. But as an Isabelle user I'd add in that I suspect the fact that no further work builds on the sheaves definition in Isabelle currently is more to do with a lack of Isabelle people working in algebraic geometry compared to Lean, then usability of the library itself. I personally find locales very natural to work with in other areas of mathematics (worth noting my own biases here as my libraries are built with them!), and am yet to come across something where I feel I need dependent types. Are there a few things which I suspect may be slightly easier with dependent types, yes, but there are other cases where the lack of dependent types can keep things simple and lead to some nice features, also yes (e.g. level of automation through Sledgehammer).

A little added background on Isabelle's algebra libraries and general usability. HOL-algebra (which is in the distribution, not the AFP, and contains the typeclass definition of rings) is pretty old at this point, but also pretty expansive. In 2020, Ballarin first suggested using locales for formalising algebra more naturally, which was then put on the AFP, and quite a number of new developments have now used that. I know theres been a bit of talk about redoing HOL-algebra using this locale approach entirely, but that's obviously a decent undertaking. Given typeclasses in Isabelle also effectively contain a locale, I'm pretty confident you could connect the two formalisations via various locale mechanisms relatively easily and lift various definitions (if someone hasn't done this already) in the meantime.

Personally, I think the differing choice between Isabelle and Lean nowadays is less dependent types centric, but more about what you want out of the library and proof assistant. Purely looking at this from a library perspective, Lean offers a pretty amazing library that is completely interconnected, which (from my understanding) means you don't have the issue of competing versions, everythings interconnected, and theories tend towards very general definitions. This can make it pretty nice to work across different areas of mathematics, which is a definite advantage. Alternatively, Isabelle doesn't subscribe to having a monolithic library, instead having the core distribution and an archive (AFP). This means that people can formalise things in different ways (from very general, to more surface level) and so you have more choice depending on various use cases which can also be nice. That's not to say you can't connect separate libraries (and there are several tools to help with this) to benefit from past work if needed, it may just (in some cases) not be as natural as when everything is interconnected. Personally, my work used several different areas of mathematics together relatively easily so this is topic dependent.

In contrary to the point just posted, I would argue that in Isabelle you can still create very general libraries which absolutely still offer similar advantages in uncovering overlooked details and achieving a deeper understanding of a subject. I think this is an advantage of proof assistants generally for mathematics, and no matter what tool people are using its great to see it happening!

[Utensil Song]

My impression of Isabelle is that although it's based on type theory, it has done a great job mimicking the set-theoretical mindset, thus it seems usually more straight forward to convert an informal text into Isabelle, and reading Isabelle code has better correspondence with the informal text, this is in contrast of reading Lean code, one frequently runs into a situation that some context of the design choices need to be learned, and that was to handle some peculiar issues from DTT.

Judging by reading Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types, locales seem to be a great mechanism to mimicking the set-theoretical mindset in a complex theoretical context, as they are predicates that could carry parameters, data, and supports multiple inheritance. But I would suspect that it would run into issues similar to (although technically different) Lean faced when it's used in a scale like Mathlib. The situation of automation in Isabelle can greatly help fighting these issues, though Lean would also get there in near future.

[Chelsea Edmonds]

I think there's some truth re the set theoretical mindset there (particularly when using locales). Its worth noting though that the format of Isabelle code being more readable has little to do with this. Isabelle has a tactic based language (similar to Lean), but for longer proofs in mathematics most people use Isar - a structured proof language with that better correspondence to informal text, which for some reason an equivalent hasn't really even taken off in Lean. This is a proof assistant feature that has little to do with foundations, and its admittedly one of the things I do miss when working in Lean compared to Isabelle!

Definitely, scalability of large libraries with locales also has its own technical challenges. It's always interesting comparing the similarities of challenges (but also differences) in formalisations across systems! I would say based on talking to people in the automation community (not an expert in this at all myself!) that dependent types do make automation in Lean more challenging, so I'm not sure if it'll ever be completely equivalent to whats available for HOL, but theres definitely a lot of working going into improving it which is great to see.

[Bulhwi Cha]

So, I guess there are some proof assistants besides Lean that people can use to create a monolithic general-purpose mathematics library without too much pain.

[Chelsea Edmonds]

Bulhwi Cha said:

So, I guess there are some proof assistants other than Lean that people could use to create a monolithic general-purpose mathematics library without too much pain.

With the right community (which is ultimately what Lean has done amazingly well for mathematics) and infrastructure (e.g. well-managed gitrepo), I personally believe so. That said, I'll absolutely defer to Mathlib maintainers as to what 'too much pain' means when it comes to creating and maintaining such a large library of formal mathematics!

[Ruben Van de Velde]

Yeah, I think community norms and focus are probably at least as important as the language itself

[Shreyas Srinivas]

With different communities and ITPs come different proof styles. As a mainly lean user, I still haven't wrapped my head around the whole idea that one must transform the proof state and bring it to a point where big automation (auto, sledgehammer, blast etc) can solve it. These days I find myself automatically preplanning my proofs based on what I think I can get lean (or sometimes Rocq) to do, and I understand the end result better even if it is longer, and can also repair it between breaking lean changes with a bit of zulip community help. Another thing is not having named hypothesis. There are also UX issues. But this is a very lean-biased perspective. I have heard from Isabelle users who say that its SMT integrations are very useful in formal verification of low level systems details. Less modularity is required. And of course community matters a lot. I have been advised at least on two separate occasions that being in Munich or Cambridge is very helpful when working on Isabelle.