Mark Wassell (Oct 12 2020 at 08:08): 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
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
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.
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
Manuel Eberl (Oct 12 2020 at 10:12):Uh, you mean linear optimisation, right?
Lukas Stevens (Oct 12 2020 at 10:13):What did you think of?
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.
Lukas Stevens (Oct 12 2020 at 10:14):Yes, you need some results from convex geometry to do linear optimisation
Lukas Stevens (Oct 12 2020 at 10:16):Linear optimisation also forms the basis for discrete optimisation.
Lukas Stevens (Oct 12 2020 at 10:17):The slash was meant as convex geometry and linear optimisation
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."
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
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).
Angeliki Koutsoukou-Argyraki (Oct 13 2020 at 07:07):It shouldn't be too difficult to infer such a list from the Isabelle libraries
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.
Manuel Eberl (Oct 13 2020 at 19:26):Yeah I was mostly thinking of the high school stuff. Trigonometry etc.
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.
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: Apr 18 2024 at 20:16 UTC