Lean 4 link / implementation

[felixpernegger]

(This would be more appropriate in the web repo but realistically it wont be seen there, X-post with Zulip #pi-base > Lean linkage @ 💬)

I wrote about this before in #1506, a good version of this is at https://github.com/pi-base/data/tree/lean-sandbox (from 1.5 years ago). Also see https://code4math.zulipchat.com/#narrow/channel/416467-pi-base/topic/Lean.20integrations/with/406960871

For many different reasons, having (a link to) formal proofs for theorems would be great. Among others:

• Since pibase is genuinely at a point where almost all reasonable "theorems" from general topology are in the deduction engine, this would be a very natural place to expand, especially considering current trends.

• As a small heuristic, even if we assume each theorem in pi-base has a 99.8% chance of being stated correctly, this only leaves a 18% chance of all theorems being correct, thus formal verification would be very useful.

• A formalisation effort could also attract new people to pibase.

• On the other side, for the development of general topology in Lean/mathlib, pi-base would be an amazing source.

There are a few different ways to set up a connection, but I think the best way would be the following: Have a separate repo with theorems and properties (possibly spaces but im not a fan of this too much) formalised in Lean and have the website automatically link to a formalisation if it exists (i.e. if a folder "T123" exists in the Lean repository, the website say "Formalisation available at (link)".
This is what is being done at the popular Erdos problems website, see for example here.
I would be more than happy to set something like this up, I do not think this would be especially challenging at all.

I made a repository in this regard where I formalised almost a 100 properties of pibase (though not always super polished, this would need to be checked more carefully) and (as a test) 3 theorems.

In any case, I'd really appreciate any feedback for this (last time this didnt happen all too much). :)