Where is Kevin when you need him?

Stream: new members

[Eric Taucher]

@Kevin Buzzard
New StackExchange question.
Are some proof assistants better suited for given areas of math than others? (ref)

[Anatole Dedecker]

I’ve learned to fear that kind of questions…

[Arthur Paulino]

One thing I would honestly like to know is: what are the hard thresholds of known proof assistants?
That is:

• What can't Lean do?
• What can't Coq do?
• What can't Agda do?
  ...

[Adam Topaz]

The answer: Kevin is probably in London, where it's after midnight.

[Adam Topaz]

@Arthur Paulino that sounds like a perfect question for the stack exchange!

[Arthur Paulino]

Gonna post it in a few minutes

[Kevin Buzzard]

Eric Taucher said:

Kevin Buzzard
New StackExchange question.
Are some proof assistants better suited for given areas of math than others? (ref)

OK OK I answered.

[Eric Taucher]

I saw, I upvoted. If I had written it I would have accepted.

[Will Sawin]

Is anyone really afraid that there are foundational issues preventing one from defining the tensor product of two vector bundles in Lean?

[Eric Taucher]

Will Sawin said:

Is anyone really afraid that there are foundational issues preventing one from defining the tensor product of two vector bundles in Lean?

Can you ask that as a new question.

[Eric Taucher]

I really didn't expect this get this much attention and really do not need it to grow any more.

[Eric Taucher]

I would close this topic but I don't know if that is possible with Zulip.

[Kevin Buzzard]

@Will Sawin there is more to this than meets the eye [more to come]

[Kevin Buzzard]

It might be easier to explain the schemes in HOL situation first. Isabelle/HOL doesn't have dependent types, but it can try to work around this. A sheaf of commutative rings wants to eat an open set and spit out a ring. Sounds like it's a function, right? But if it's a function, what is the codomain? There's no set of all rings. A sheaf is of course a functor, not a function, and this concept doesn't fit into HOL. So what can one do in practice? What one can do is to fix a specific sheaf (e.g. the structure sheaf of some scheme) and then take the disjoint union of all the O_X(U) as U varies over all the open sets and call this thing R, and then you can define the structure sheaf as a function from the set of open subsets of X to the set of subsets of R. Now this thing is a function again. The problem is that rings are supposed to be types, and a subset of R is not a type, it's a term. Moreover R is not a ring; it has many 0s, many 1s, and a weird partially-defined multiplication. Isabelle/HOL's ring theory is not set up to work with either R or its subsets, so they had to redesign ring theory so as to allow subsets of R to be rings. And now the problem is that the theory of tensor products of modules over a ring all has to be rewritten etc etc if you want to do tensor products of O_X-modules. Is it possible in theory? Probably. Will it actually compile in finite time if you try it in practice? Who knows -- this is an unsolved problem.

[Kevin Buzzard]

OK so now let's move onto Lean. Consider complexes of abelian groups indexed by the integers. This is easy, right? We have A : Z -> Type (Lean can do this) and for each i, A(i) gets an ab gp structure, and then for each i we have d(i) : A(i)->A(i+1) and the axiom that d^2=0. What could go wrong? Rather surprisingly, when you start looking at homotopies and things you end up looking at d(i-1):A(i-1)->A((i-1)+1) and guess what: A((i-1)+1) and A(i) are not considered particularly equal by Lean, because (i-1)+1 and i are propositionally equal but not defniitionally equal. Lean can come up with an isomorphism from A((i-1)+1) to A(i) but it's not an equality. All of a sudden there are tons of isomorphisms floating around which you have to keep track of. Now try and prove that a short exact sequence of complexes induces a long exact sequence in cohomology. It's horrible. Can it be done in theory? Maybe. Can it be done in practice? I don't know, because after a lot of thought we came up with a fix where we don't have d(i):A(i)->A(i+1), d instead takes three inputs i, j, and a proof that j=i+1, and spits out a map from A(i) to A(j). This solves the problems. But this problem needed solving; without it it was going to be absolute hell to do homological algebra; some insight was needed here.

[Kevin Buzzard]

If that's the situation with complexes of sheaves of abelian groups over a point, now imagine what happens when you put these two things together and start doing complexes of sheaves of abelian groups, and trying to do homological algebra with them. Equality in type theory is hard. There are lots of things which mathematicians think are equal but which are not equal, e.g. for sure you can't have all of $\R^2\times\R=\R^3=\R\times\R^2$ being true at once, and in Lean none of these are equal. This sounds like just some stupid observation but now try proving that the product of two real manifolds is a manifold -- this issue is real, and I don't know if we have products of manifolds yet. Problems like this can compound themselves and after a while you can drown. Right now smart people are working out how to deal with these issues, but at the end of the day the point is that mathematicians have an extremely fluid idea of equality, Lean has an extremely precise idea, and then when the ideas don't coincide then you either have to think hard about how to make things more Lean-equal, or you have to bite the bullet and start carrying around invisible isomorphisms, and the moment you have too many of these things writing code gets slower and slower.

[Kyle Miller]

Kevin Buzzard said:

we came up with a fix where we don't have d(i):A(i)->A(i+1), d instead takes three inputs i, j, and a proof that j=i+1, and spits out a map from A(i) to A(j).

I'd run into this problem, too, when trying to prove some things about inverse systems of types. The solution I came up with was to work instead with inverse systems of sets on a "universal" type. It's not quite so clear how you'd want to set this up for abelian groups, but it could be done (have a single abelian group A, an endomorphism d : A -> A, a grading g : A -> Z, and axioms that d^2 = 0 and that d shifts the grading by 1), while surely pushing some problems elsewhere.

"Buffering" a definition with an equality seems like a useful idea. One thing I wonder is what the difference is in practice between buffering the inductive type or providing an additional buffered interface. (Certainly, having two d operators makes things more annoying since rewrites for one don't apply to the other...)

structure cplx :=
(α : ℕ → Type)
(d : Π (i : ℕ), α i → α (i + 1))

def d' (c : cplx) (i j : ℕ) (h : i + 1 = j) : c.α i → c.α j :=
by { subst h, apply c.d }

[Johan Commelin]

One caveat is that you might want to talk about a complex of foos where the category of foos doesn't have countable coproducts.

[Kyle Miller]

I haven't tried doing any homological algebra with it so it is very untested, but just to give something closer to what I was doing with having a universal type, rather than using the coproduct trick (which doesn't always work), there's this:

structure cplx (α : Type*) :=
(A : ℤ → set α)
[inst : Π (i : ℤ), add_comm_group (A i)]
(d : Π (i : ℤ), A i →+ A (i + 1))

instance (α : Type*) (c : cplx α) (i : ℤ) : add_comm_group (c.A i) := c.inst i

Even though there are those subtype coercions in there for d, when you're manipulating elements you can lean on the crutch of cracking everything open to get terms of α. (I didn't need typeclasses to work, however, so I worry by doing this you can easily lose track of the add_comm_group structure...)

[Will Sawin]

@Kevin Buzzard Thanks for this detailed explanation! I still have two questions:

(1) When you say "after a while you can drown", I get that, but we're not talking about "after a while", right? In a traditional textbook the product of manifolds might be defined directly after manifolds are defined and a few examples are given. Tensor product of vector bundles can be defined right after vector bundles if you want. Keeping track of that isomorphism sounds annoying but, in the proof that the product of two manifolds is a manifold that I know, it's only used once, to construct another isomorphism. Is the point less that it might not be possible even if someone grits their teeth and writes down a bunch of isomorphisms and more that it might not be possible in a way that produces clean code that is up to your standards?

(2) When you say maybe something can't be done, are you not comforted by the fact that other, seemingly much more difficult things can be done? Wasn't that the whole point of constructing perfectoid spaces? Do you think that after the Liquid Tensor Experiment finishes with a proof of Theorem 9.1 from Clausen-Scholze, no one will be able to extend it to Theorem 6.5 because it's too difficult to define tensor products of sheaves?

[Patrick Massot]

He means you can drown if you isomorphism pile up and get out of control.

[Patrick Massot]

We very much hope that there is no fundamental obstacle to formalizing everything, but it requires work.

[Will Sawin]

For products of manifolds, isn't that some combination of https://leanprover-community.github.io/mathlib_docs/geometry/manifold/smooth_manifold_with_corners.html#model_with_corners.range_eq_univ_prod and https://leanprover-community.github.io/mathlib_docs/geometry/manifold/smooth_manifold_with_corners.html#model_with_corners.range_eq_univ_prod ?

[Patrick Massot]

We have products of manifolds, but it requires more work than what you think it should.

[Kevin Buzzard]

Tensor products of sheaves will probably get done somehow, and hopefully they'll be usable. It's not just about making the definition, it's about proving theorems about the definition. If we have products of manifolds now, do we have that $X\times Y$ and $Y\times X$ are diffeomorphic? What about $(X\times Y)\times Z$ and $X\times (Y\times Z)$? These are not idle questions -- mathematicians will inevitably use these facts and they might be really painful to prove. Are they impossible to prove? Hopefully not. But such silly things can present genuine impediments to progress, and when you run out of people who are prepared to put the time and effort into doing them -- when our small pool of volunteers becomes a set of size 0 -- then you're stuck. And you're also stuck (as Johan was a while ago with Witt vectors) if the software decides to start timing out on you, not finding the route to something which you think it should be doing automatically, or taking a long time to find it. We only got Witt vectors in part because Gabriel Ebner actually rewrote a part of core Lean 3 so that it worked better. It is not a given that MSR will randomly rewrite parts of core Lean 4 just because we're stuck on something. It should all work in theory, but whether things work in practice is a different kettle of fish. Things can get unexpectedly complicated sometimes, and it then takes either a good solution from a mathematician or a good solution from a computer scientist before things can get back on track.

[Adam Topaz]

The product of manifolds could be a good example of isomorphism overload. If you define $X \times Y$ as the usual (type-level) product with the appropriate manifold structure, that's great, but of course one should also prove that this is indeed the product in the category of manifolds. Once one has that, you could write prod X Y where prod refers to a noncomputable docs#category_theory.limits.prod and then use general nonsense to obtain an isomorphism between prod X Y and prod Y X. The uniqueness of limits would then give you isomorphisms between the actual product you constructed before and this noncomputable prod X Y, so you could compose three isomorphisms to obtain an isomorphism between X x Y and Y x X. Now you have to work with such an isomorphism whenever you want to interchange X and Y in your "explicit" product, and it only gets worse from there. (This example is a bit contrived, because it's possible to avoid going through the noncomputable stuff, but in other situations this might be the best approach.)

[Jay Sulzberger]

Perhaps the systematic use of functors, functors between different proof assistants, might help. One might define a few score proof assistants which are not part of Lean. Then prove various transports and theorems, ah, "metatheorems", that justify source to source translations, from, say, a little proof assistant that handles Universal Algebra, style of G. Birkhoff's HSP Theorem on Varieties, to/from Lean.

Likely something like this has already been done inside Lean.