Stream: General

Topic: Undergraduate mathematics in Isabelle


view this post on Zulip Mark Wassell (Oct 12 2020 at 08:08):

Hello,

You have probably seen this article in Quanta

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001

and there is a response from the Coq community on Zulip here

https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Quanta.20Magazine.20article.20on.20formalized.20math.20libraries

Lean has a list of undergraduate mathematics topics that have been formalised in it.

https://leanprover-community.github.io/undergrad.html

Is there such a list for Isabelle?

Mark

view this post on Zulip Manuel Eberl (Oct 12 2020 at 09:51):

I don't think there is. We could definitely do something like that. I'd have to look into how they organise their list. Are they using some standard undergraduate textbook for the categorisation?

I think we should have a fair amount of undergraduate logic, real and complex analysis, ODEs, number theory, analytic number theory, measure theory, probability theory. Algebra is a bit lacking (e.g. we don't have any Galois theory and not much ring theory, although advanced ring theory is perhaps not undergraduate material anyway).

We don't have a lot of geometry. Geometry in a theorem prover is always a bit annoying, except for the very rigorous and formal kind (like what you do in finite geometry). The typical ‘high school geometry’ problems tend to get pretty annoying though.

I don't think we have any algebraic geometry. It could be done, but I think our multivariate polynomial library would need a big overhaul. Whenever I use it, I keep running into missing basic material, and the material we do have is spread over like half a dozen AFP entries (which is in part also my fault).

Other areas where we don't have much (or nothing at all) are game theory, PDEs, statistics, optimisation.

Two areas where we have quite a bit but it could be better and more systematic are topology and combinatorics.

view this post on Zulip Lukas Stevens (Oct 12 2020 at 10:03):

There is at least some basic convex geometry/optimisation since the simplex algorithm is formalised: https://www.isa-afp.org/entries/Simplex.html

view this post on Zulip Manuel Eberl (Oct 12 2020 at 10:12):

Uh, you mean linear optimisation, right?

view this post on Zulip Lukas Stevens (Oct 12 2020 at 10:13):

What did you think of?

view this post on Zulip Manuel Eberl (Oct 12 2020 at 10:13):

You said ‘convex geometry/optimisation’. I read that as ‘convex geometry/convex optimisation’. Convex optimisation is a thing, but more general than what Simplex does.

view this post on Zulip Lukas Stevens (Oct 12 2020 at 10:14):

Yes, you need some results from convex geometry to do linear optimisation

view this post on Zulip Lukas Stevens (Oct 12 2020 at 10:16):

Linear optimisation also forms the basis for discrete optimisation.

view this post on Zulip Lukas Stevens (Oct 12 2020 at 10:17):

The slash was meant as convex geometry and linear optimisation

view this post on Zulip Mark Wassell (Oct 12 2020 at 10:22):

From the Coq Zulip discussion: "The [Lean] mathlib website generates that page from a yaml file https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml. The list of topics was extracted from some version of the standard French undergraduate curriculum, linked in the yaml."

view this post on Zulip Mark Wassell (Oct 12 2020 at 10:22):

The list of topics is from http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf

view this post on Zulip Anthony Bordg (Oct 12 2020 at 16:54):

Manuel Eberl said:

We don't have a lot of geometry. Geometry in a theorem prover is always a bit annoying, except for the very rigorous and formal kind (like what you do in finite geometry). The typical ‘high school geometry’ problems tend to get pretty annoying though.

We have at least some projective geometry (the "rigorous and formal kind", i.e. axiomatic).

view this post on Zulip Angeliki Koutsoukou-Argyraki (Oct 13 2020 at 07:07):

It shouldn't be too difficult to infer such a list from the Isabelle libraries

view this post on Zulip Mohammad Abdulaziz (Oct 13 2020 at 10:13):

@Manuel Eberl I don't really know what you mean by 'optimisation', but for combinatorial optimisation, which is a major area of applied undergrad maths, we have a lot of major results: we have Edmonds' blossom and Edmonds-Karp algorithms, and, hopefully soon the Hopcroft-Karp algorithm. Also, the simplex algorithm is a major result of discrete optimisation. I think we also have the weak duality theorem.

For PDEs, we don't have any formalised methods for solving them, but we have Green's theorem which can be used for reasoning about and solving some PDEs.

view this post on Zulip Manuel Eberl (Oct 13 2020 at 19:26):

Yeah I was mostly thinking of the high school stuff. Trigonometry etc.

view this post on Zulip Manuel Eberl (Oct 13 2020 at 19:28):

Mohammad Abdulaziz said:

Manuel Eberl I don't really know what you mean by 'optimisation', but for combinatorial optimisation, which is a major area of applied undergrad maths, we have a lot of major results: we have Edmonds' blossom and Edmonds-Karp algorithms, and, hopefully soon the Hopcroft-Karp algorithm. Also, the simplex algorithm is a major result of discrete optimisation. I think we also have the weak duality theorem.

For PDEs, we don't have any formalised methods for solving them, but we have Green's theorem which can be used for reasoning about and solving some PDEs.

I guess in my mind, the things you mentioned are classified as ‘graph theory’. When I said ‘optimisation’ I was more thinking of the non-discrete stuff: linear optimisation, convex optimisation, and non-linear optimisation, because I took an entire course on that.

Of course, I also had discrete optimisation in my maths undergraduate degree, but that was in a lecture called ‘discrete mathematics’, so I didn't really mentally associate it with optimisation I guess.

view this post on Zulip Mohammad Abdulaziz (Oct 14 2020 at 08:49):

Some, but not all (e.g. LP duality), of these results are described in general algorithms books as part of graph algorithms, but usually without proofs or depth, in the same way general algorithms books might discuss cryptography, etc. These algorithms are, however, properly described and studied in combinatorial optimistation books and courses, which are classified by different universities (e.g. TUM) and other bodies (e.g. AMS) as applied maths. Of course, these classifications are arbitrary, and you don't necessarily have to agree with them. But my point is: they are taught in standard undergrad maths courses as combinatorial optimisation.


Last updated: Aug 15 2022 at 04:16 UTC