Formalizing topology.pi-base.org

Stream: general

[Steven Clontz]

Moving a conversation from email among myself, @Katja Berčič, and @David E. Narváez that might be useful to have open to the community:

My (naive!) vision for one day formalizing topology.pi-base.org is to have Lean code (probably depending on mathlib) for the following four models:

• Spaces: defineinstance : TopologicalSpace S123
• Properties: define class P123 (X : Type u) [TopologicalSpace X] : Prop
• Theorems (each of the form $P1\wedge P2\wedge ... \rightarrow P3$): prove theorem T123 [P1 X] [P2 X] ... : P3 X
• Traits (space/property pairs S123:P456): prove instance : P456 S123

My motivation is internal: I want to be able to note on our web application which of our results have been formally proven vs. informally proven. But I'm quite interested in how this work might be helpful upstream to mathlib as well. E.g. a standard result like https://topology.pi-base.org/spaces/S000025/properties/P000036 is hopefully a one-liner from mathlib. But something more esoteric like https://topology.pi-base.org/theorems/T000726 would require a lot of novel code beyond mathlib, but having it in our database means it could be used by other formalization projects as needed in the future.

Does that make sense?

[Aaron Liu]

I remember there being previous discussion along these lines

[Aaron Liu]

ah yes here it is #mathlib4 > Some missing, accessible, topology results @ 💬

[Kevin Buzzard]

This sounds like a great idea for a standalone repo with mathlib as a dependency.

[Michael Rothgang]

Continuing a thread hinted at in the past thread: I think having some overview of formalised vs. unformalised implications would be really nice. The 100 and 1000+ theorem pages do something similar; I wrote some infrastructure for doing a bi-directional sync here. Happy to share what I learned!

[Steven Clontz]

@Kevin Buzzard absolutely. I think it should be part of https://github.com/pi-base/data/ and be represented on https://topology.pi-base.org . Actually I now remember that I very briefly played around with the idea a year ago at https://github.com/pi-base/data/pull/672

[Steven Clontz]

@Michael Rothgang what do you mean by "100 and 1000+ theorem pages"?

[Steven Clontz]

Another relevant thread that's coming to mind from before: https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/general.20topology.20in.20mathlib

[Ruben Van de Velde]

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

[Michael Rothgang]

And https://leanprover-community.github.io/1000.html, which cross-references mathlib statements with the theorems collected at https://1000-plus.github.io/