This aims to formalise the properties and theorems from the π-Base in Lean 4. A motivation for this is found here.
Any property and theorem should have abbreviations, see property P37 and theorem T39 as examples.
To contribute please open an issue and then a PR. Note we are strictly using the definitions from pi-base and not mathlib in cases they differ.
As of writing, this project is still in its infancy, so the structure of the repo etc. might and probably will change later.
The project dashboard tracks the formalisation against π-Base and hosts the open-implications workflow of felixpernegger/pibase-data.