Lean formalisation.

[felixpernegger]

I am sure this has been discussed to some degree before (something similar is even mentioned in the original announcement of $\pi$-base 11 years ago), however I did not find any concrete discussions.

It would be of great use to formalise the properties in $\pi$-base and theorems connecting them in Lean and reference this on the website. Some reasons:

• Most importantly, we do not have to worry if theorems are actually correct once they are formalised. Therefore one can add many "trivial" theorems as well, which would otherwise be avoided.
• Lean supports typeclass inference, so the deductions automatically performed in $\pi$-base would likely work in Lean as well
• At least to my understanding, formalisation is a rapidly growing topic in mathematics, therefore it would be natural to follow this current trend
• Much of topology is already formalised in Lean's mathematical library mathlib. On the other hand $\pi$-base could potentially be a roadmap for formalisation of general topology

and many more reasons. It is furthermore not difficult_. As a proof of concept, I formalised the first 30 properties in $\pi$-base in Lean, see this. Admittedly, most of them were in mathlib already, which would not be the case with most of the latter properties, nevertheless I doubt (first outline) a formalisation of all properties would take more than say two weeks (possibly excluding the few properties related to algebraic topology). The way I approached it in this file is one of many, probably not ideal, though I do not think it matters very much.

I think the most natural way to include Lean in the current website, to do it similarly as the erdos problems website, see for example this. That is, to each theorem and property (and potentially space/trait) add a statement/link whether it has been formalised or not. If it has, just give a link to the formalisation. Preferably all collected theorems should be in a shared repository I guess. Later one could try to integrate formalisation more naturally to the website, but I think that would be a good start, which could be done (I think) very quickly.

One could also formalise the spaces and their traits in $\pi$-base, though I think that far less useful at this point compared to theorems and properties.

I am still quite new to $\pi$-base, so I really appreciate any comment!

[yhx-12243]

There are some branches which have some attempt for this, e.g., https://github.com/pi-base/data/tree/lean-sandbox and https://github.com/pi-base/data/tree/jcd/mathlib.