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

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

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.

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

Uh, you mean linear optimisation, right?

What did you think of?

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.

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

Linear optimisation also forms the basis for discrete optimisation.

The slash was meant as convex geometry and linear optimisation

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."

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

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).

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

@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.

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

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.

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