Lean integration proof of concept

pi-base / data

A community database of topological counterexamples

https://topology.pi-base.org/

Creative Commons Attribution 4.0 International

72 stars 24 forks source link

Lean integration proof of concept #672

Closed StevenClontz closed 2 weeks ago

StevenClontz commented 3 months ago

Toying around with a model suggested by @erdOne at https://github.com/leanprover-community/mathlib4/pull/12387#issuecomment-2075877674

StevenClontz commented 3 months ago

Curious what you think @jamesdabbs. Since I don't think we're going to get all of pi-Base into mathlib anytime soon (their contribution loop is rather slow and I don't think there's interest in including many of the "pathological" examples we like in general topology), this is a possible way for folks to formalize the results we assert (and our build process can confirm which results have been formalized for display in the viewer app).

StevenClontz commented 2 weeks ago

Closing as stale for now.