Zulip Chat Archive

Stream: maths

Topic: Stokes' theorem


view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:37):

Occasionally I run into people who say "what is all this fuss about getting all of an undergraduate(UG) curriculum into Lean, basically this was already done by Mizar and pretty much all of it is in Coq". I would always forcefully argue that this was not the case -- just because there is a bunch of UG maths in these systems does not mean we have a full UG curriculum. My standard counterexample was finiteness of class group of a number field, and in fact I could even twist the knife by observing that even though some of these provers have been around for 30 or 40 years, none of them even had the definition of the class group of a number field, something which was in certain cases known to Gauss.

But I see in my ArXiv daily posting today that I am now out of date -- congratulations to Anne, Sander, Ashvni and Filippo, who have proved the class group of a number field is finite in Lean. At Imperial we also teach the result about finite generation of the unit group (this is a far-reaching generalisation of the theory of the Pell equation, at least if you state precisely how many generators the unit group has), but this result certainly looks very accessible now. My other standard counterexample was insolvability of the quintic, but this is now done in Coq by Cyril and Assia and others, and people who follow the #Berkeley Lean Seminar stream will know that they're well on the way to doing this in Lean too.

So I need a new taunt, and I'm going for Stokes' theorem, in the form I learnt it in my final year UG course, which was for smooth manifolds with boundary -- the "Stokes-Cartan" or "generalized Stokes theorem" here.

How far are we from having this in Lean? And is this already done, or being worked on, in other theorem provers?

Once this is done, we are perhaps getting to the point where perhaps the union of all theorem provers really does look like it covers the vast majority of an undergraduate pure mathematics degree (of course we can then start talking about MSc's...).

view this post on Zulip Mario Carneiro (Feb 05 2021 at 18:42):

Complex analysis is covered in isabelle and HOL Light but I don't know how comprehensive it is; that might be another example

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:47):

I am just assuming that all complex analysis is done in these HOL systems, however my impression is that their ability to work with complex manifolds is not good, so perhaps another candidate theorem is the statement that a non-constant map between two compact Riemann surfaces has a degree, a weak form of which would be the statement that there exists some positive integer d such that away from a finite set in the target, the pre-image of a point in the target is d points in the source.

view this post on Zulip Mario Carneiro (Feb 05 2021 at 18:48):

what undergraduate learns that though?

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:49):

I learnt that in the 3rd year Riemann surfaces course

view this post on Zulip Mario Carneiro (Feb 05 2021 at 18:49):

I suppose riemann surfaces are covered in a complex analysis course?

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:49):

@Bhavik Mehta is this still taught in Cambridge, do you know?

view this post on Zulip Mario Carneiro (Feb 05 2021 at 18:50):

My university didn't have anything more specialized than "complex analysis"

view this post on Zulip Mario Carneiro (Feb 05 2021 at 18:50):

for undergrads, at least

view this post on Zulip Bhavik Mehta (Feb 05 2021 at 18:51):

Yeah, Riemann surfaces are a third-year undergraduate course in Cambridge

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 18:51):

UK universities might be more specialised, because they are catering for people who were only doing maths and two other subjects since the age of 16 and are only doing maths courses from 18 onwards. The UK UG system is more high-powered than the US system in general. On the other hand the US PhD system is much better than the UK system, where funding runs out after 3.5 years and you're expected to basically have a thesis by then. In the US I think the average is more like 5 years. In the UK you start with an advisor on day 1.

view this post on Zulip Johan Commelin (Feb 05 2021 at 19:08):

I saw the degree of maps between Riemann surfaces before finishing my BSc

view this post on Zulip Heather Macbeth (Feb 05 2021 at 21:02):

@Yury G. Kudryashov has a baby version of Stokes' theorem, not yet PR'd. (It's for boxes in Rn\mathbb{R}^n.). And in Isabelle they have Green's theorem, for some kind of domain (C^1 or piecewise C^1?) in the plane.

view this post on Zulip Heather Macbeth (Feb 05 2021 at 21:03):

But for "proper" Stokes' theorem, on manifolds, we'll need, among other things, a fully functioning library for tensors on manifolds. At the moment we don't even have the definition of a vector bundle ... unsurprisingly, it's not easy!

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 21:08):

Yes I'm very very well aware that it's not at all easy. This is why it's a good challenge. I know we have Patrick's formalised definition of an UG degree (which is a very precise list of things showing up in one specific degree taught in France) but if you're prepared to use the more flexible one of "whatever someone in Cambridge or Harvard or Princeton or any one of 100 other decent institutions teach in the first three or four years" (which is I think a definition that most people in maths departments would agree was a reasonable interpretation of "an undergraduate degree") then we can see that there are still a few serious challenges left. Good challenges drive the area forwards of course.

view this post on Zulip Adam Topaz (Feb 05 2021 at 23:45):

Heather Macbeth said:

But for "proper" Stokes' theorem, on manifolds, we'll need, among other things, a fully functioning library for tensors on manifolds. At the moment we don't even have the definition of a vector bundle ... unsurprisingly, it's not easy!

I thought there was a PR for vector bundles somewhere?

view this post on Zulip Adam Topaz (Feb 05 2021 at 23:45):

I remember discussing this.

view this post on Zulip Adam Topaz (Feb 05 2021 at 23:46):

#4658 looks like it hasn't been touched in a little while. (and it's for topological vector bundles)

view this post on Zulip Yury G. Kudryashov (Feb 06 2021 at 01:50):

I'm going to rewrite my Stokes theorem to require only integrability instead of continuity, then PR it.

view this post on Zulip Eric Wieser (Feb 06 2021 at 08:28):

#4658 looks like it has a bunch of typeclass relaxations for dual that should be cherry picked

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 08:57):

I bet we assumed continuity in my UG course but unfortunately all the notes are in my office and we're in lockdown in the UK...

view this post on Zulip Filippo A. E. Nuccio (Feb 06 2021 at 17:34):

Thanks Kevin! You mention Dirichlet's Units Theorem: indeed, we thought about this as a possible future project, we mention this in the closing remarks. We will see...


Last updated: May 09 2021 at 11:09 UTC