Integration of pi-Base and Lean

[StevenClontz]

@jamesdabbs @kisonecat

Jim shared with me this repository: https://github.com/kisonecat/pi-base-mathlib

I haven't had time to look closely but wanted to connect you two (you'll both be at AIM in a few weeks).

[StevenClontz]

Is there a way to take the string T2Space and produce a URL to a webpage that represents it as part of mathlib? I can find https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Separation.html#T2Space manually, but it includes a Separation.html# prefix.

[StevenClontz]

I suppose https://leanprover-community.github.io/mathlib4_docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=T2Space would be better than nothing.

[kisonecat]

I asked on the Lean Zulip, which led to my writing

https://github.com/kisonecat/pi-base-mathlib/blob/main/PiBase/Property.lean#L99-L103

which will take a name like T2Space and automatically produce the appropriate URL; these will be updated if something gets mvoed around mathlib. As an example of this, running

#eval findDocumentationURL "T2Space"

correctly produces the link https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Separation.html#T2Space

Running pibase verify currently just prints out these URLs. The output of pibase verify could be used to build the website. The reflection and metaprogramming facilities of Lean are really nice.

[StevenClontz]

Cool. I think this would be a neat project to hack on at AIM in a few weeks.

[jamesdabbs]

Working towards landing this in #478

[StevenClontz]

Dropping a thought here - James has threatened to use Lean for compiling the data repo, but it would be ideal if compilation could happen in the browser. In particular it'd be great if a VS Code plugin could run within a browser instance of VS Code to provide immediate feedback to contributors without having to run CI on a pushed commit.

[kisonecat]

With kisonecat/pi-base-mathlib@c98551e there is now a dump subcommand that outputs Lean code. This provides abbrevs for each property and dumps out the signature of all theorems for which hypotheses and the conclusion have mathlib: links. For example, running pibase dump outputs

-- "$T_3$"
abbrev P000005 := T3Space

-- Completely regular
abbrev P000012 := CompletelyRegularSpace

-- "$T_4$"
abbrev P000007 := T4Space

-- "$T_{2 \\frac{1}{2}}$"
abbrev P000004 := T25Space

-- "$T_2$"
abbrev P000003 := T2Space

-- "$T_5$"
abbrev P000008 := T5Space

-- "$T_0$"
abbrev P000001 := T0Space

-- "$T_{3 \\frac{1}{2}}$"
abbrev P000006 := T35Space

-- "$T_1$"
abbrev P000002 := T1Space

-- Regular
abbrev P000011 := RegularSpace

variable {X : Type*} [TopologicalSpace X]

theorem T000033 : (P000005 X) → ((P000004 X)) := by sorry
theorem T000151 : (P000012 X) → (P000001 X) → ((P000006 X)) := by sorry
theorem T000100 : (P000008 X) → ((P000002 X)) := by sorry
theorem T000119 : (P000002 X) → ((P000001 X)) := by sorry
theorem T000118 : (P000003 X) → ((P000002 X)) := by sorry
theorem T000112 : (P000008 X) → ((P000007 X)) := by sorry
theorem T000035 : (P000012 X) → ((P000011 X)) := by sorry
theorem T000098 : (P000007 X) → ((P000002 X)) := by sorry
theorem T000115 : (P000006 X) → ((P000005 X)) := by sorry
theorem T000113 : (P000007 X) → ((P000006 X)) := by sorry
theorem T000146 : (P000005 X) → ((P000011 X)) := by sorry
theorem T000149 : (P000006 X) → ((P000012 X)) := by sorry
theorem T000032 : (P000004 X) → ((P000003 X)) := by sorry
theorem T000148 : (P000011 X) → (P000001 X) → ((P000005 X)) := by sorry

and then the user can replace sorry with apply? to find the theorem statements in mathlib. In fact, all of these theorems are available in mathlib already!

As more properties get mathlib: links, this tool will make it easy to find theorems that are missing in mathlib.