Elementary definitions on top of mathlib's

Stream: general

[Julian Berman]

@Patrick Massot to not cloud your job posting threads, I hope it's OK to ask here about:

But there is also interesting work to do in order to make it easier to use mathlib as a backend to build more specialized libraries using more elementary definitions (for instance basing real analysis on εεε's rather than filters).

Could you say anything further about what you have in mind for this sort of thing? Or link any previous ideas you've shared that one could read? The idea(s) are to build more "understandable" undergrad-y definitions on top of mathlib's more general ones, and then what about the library of lemmas within mathlib, reproduce or re-expose those in the same more elementary mathematical language?

[Patrick Massot]

There is a very primitive example in the tutorials project. The tutorials use hand made definition for limits of sequences and functions and is mostly autonomous. However the last file (number 9) uses the Bolzano-Weirstrass theorem without proving it from scratch. There is a bit of glue here. Ideally teachers should have access to a well curated library offering elementary definitions with various glue points for advanced theorems.

[Patrick Massot]

One would need a lot more of this to allow writing exercises in calculus and integration. Managing to use mathlib of elementary linear algebra exercises is also an open question. What is in mathlib isn't optimized for elementary settings. Probably each item wouldn't require a lot of work, but someone still has to do it.