general topology in mathlib

Stream: new members

[Steven Clontz]

Having messed around with NNG and the first few chapters of mathematics in lean, I naively forked mathlib and started messing around with Separation.lean to see if could hack out some results from https://arxiv.org/abs/2312.08328 since I don't think mathlib has any separation axioms between T1 and T2.

Now, I quickly discovered I first need to go back to class and learn more about structures, classes, etc. from the textbook. No big surprise there. :-)

But once I learn how to construct the proofs I want, where should I go to coordinate with the community to make sure I'm writing a contribution that will get merged (or learn how to write an independent "library" compatible with mathlib, should these results be too niche)?

[Kyle Miller]

Separation axioms between T1 and T2 seems like a fairly niche area (I wasn't aware there were any that people studied!)

However, if this is for pi-base, it might be interesting enough to include. I would suggest not worrying too much about how you'd integrate your contributions into the main library and put all your results in a new Mathlib/New folder and checking in periodically. That way (1) you don't have to mess with making an independent library (2) all the results are in one place and you can get input about where things should go (3) it's easier to get a sense of where you're going with the library and (4) if it doesn't end up being part of mathlib, all your results are in one place and it'll be easy to make an independent library.

[Kyle Miller]

By the way, while I can't speak for all maintainers, I would welcome more topological counterexamples in the Counterexamples folder. There could be some more organization in there as well.

[Kyle Miller]

There are a handful of counterexamples inside the library itself, if I remember correctly, and they might move into that folder.

[Johan Commelin]

cc @Josha Dekker

[Steven Clontz]

So TBH I didn't study them myself until a year ago, when there was some conversation on math.stackexchange where we eventually untangled eight different intermediate properties that had been introduced in various places throughout the literature.

As you suggested, my goal there was to flesh out the pi-Base, and since these results ended up being more straightforward than my usual research, I thought it was the right place to start exploring how eventual integration of the results we track at topology.pi-base.org with mathlib might look.

[Kyle Miller]

I could imagine that there's a Counterexamples/PiBase folder with each space defined and key properties proved for each. The space might be defined inside mathlib itself, but the folder could have, for example, abbrev S000001 := Bool (I think Bool comes with the discrete topology). Then, for instances, there could be declarations like example : T2Space Bool := inferInstance to ensure that the instance exists.

[Steven Clontz]

Oh, if having a piBase corner of mathlib where we keep things wired up is something the mathlib community would be okay with, I think that's an interesting way to connect the projects.

[Steven Clontz]

@James Dabbs

[Kyle Miller]

(Maybe Archive/PiBase is better, since these aren't strictly counterexamples.)

I'm not sure that this is would be the permanent home for a PiBase project, but I think this is a great way to incubate a project, since you'll get mathlib reviewers looking at everything, and the "trade" is that formalizing PiBase database entries would naturally lead to improvements of the topology library.

[Kyle Miller]

Though maybe stick with topological properties that are 'standard', leaving niche ones to your fork?

[Josha Dekker]

So I thought of tracking the progress of PiBase automatically in Mathlib and even have a repo for this, but the code is written in Julia, and I found I didn’t know enough metaprogramming to set it up in Lean fully (which I think is important), so I sidelined the project until I know more metaprogramming. Unfortunately my own research is taking up the part of my spare time that I would’ve used on Lean, so this is kind of frozen by now. Please feel free to start afresh or get inspiration from my repo if you want to start, I won’t be able to return to this for a while I’m afraid. For what it’s worth, I’m in the progress of PR’ing k-Lindelöf spaces

[Josha Dekker]

Of course a more official integration would be much better, so I think you have a better view on how to approach this, Steven!

[Josha Dekker]

This is my repo: https://github.com/JADekker/PiBaseTracking

[Josha Dekker]

It is basically automatic conversion from PiBase files to a Mathlib-style, but it was very much WIP and low level

[Steven Clontz]

This is cool stuff @Josha Dekker. Yeah, for the sake of maintainability, writing everything in Lean itself and/or Typescript (which pi-Base runs on) would be best for a community-maintained project. I like the idea of automating things as much as possible...

[Kevin Buzzard]

I'm giving a talk called "why formalise mathematics" today and one idea I was going to mention was LLM+Lean database maybe = high level chatbot giving formally verified answers to eg questions in topology of the form "does X and Y imply Z?". Projects like this would be very helpful for that.

Of course we should really be doing counterexamples in condensed sets :-)

[Steven Clontz]

But Kevin, if such a tool exists, how will I score my easy layups on math.SE answering questions by linking to the relevant pi-Base search? :upside_down:

From a research infrastructure perspective, I really like this idea that if we find a workflow that connects databases of formally expressed examples and results into the lean ecosystem somehow, then tooling built for lean can get access to this corpus of informally proved mathematics as well.

[Patrick Massot]

You should talk to @Jure Taslak about this idea. He works on such interaction for the HOG database.

[Jure Taslak]

Hi @Steven Clontz, as Patrick mentioned, we build a Lean library for interacting with the House of Graphs database. The project is on github.

The idea of the project was two-fold, the first to be able to use the examples from the database in Lean, with verified values of their invariants and the second to double-check the values of the invariants in the database.
We build some metaprogramming scaffolding in Lean to facilitate this interaction, while also using a bit of python in the background for the actual interaction with the base (as Lean currently doesn't have HTTP capabilities as far as I'm aware).

If this sounds like something you're looking to do for pi-Base perhaps we should talk more.

[Steven Clontz]

Oh, I recognize the owner of that repo! :wave: @Katja Berčič

I think, perhaps, the goal is a little different, but maybe it's worth syncing up about at some point. In particular, HoG stores an internal representation of each of its objects. On the contrary, pi-Base only knows the asserted properties of each space, and the asserted theorems that show when properties imply others. I'm thinking that we should start storing formal representations of these things, and that this will probably be accomplished as Lean code, with a healthy amount of sorrys to fill in the spaces where things have yet to be formalized.

[Steven Clontz]

took a swing at https://github.com/leanprover-community/mathlib4/pull/12387 to explore how this might look

[Josha Dekker]

Looks good, thanks! I generated Mathlib code for many definitions and theorems for pibase, I could remove the ones that are missing and send the remainder to you, if you like?

[Josha Dekker]

I left some small suggestions by the way!

[Steven Clontz]

Josha Dekker said:

Looks good, thanks! I generated Mathlib code for many definitions and theorems for pibase, I could remove the ones that are missing and send the remainder to you, if you like?

Are these in your repo? I wouldn't mind a tour of what you've built there sometime, if you want to sync up on Zoom. There's a group talking about pi-Base on Friday if you want to join in (main topic is building a pi-Base for topos theory, but having things play nice with Lean/mathlib in the future is something I want to be mindful of)

[Steven Clontz]

Details of that call are in the https://code4math.org Zulip: https://code4math.zulipchat.com/#narrow/stream/416467-pi-base/topic/pi-base.2C.20but.20toposes

[Steven Clontz]

We also have a pi-Base community call on May 2 which doesn't have anything on the agenda yet, if you want to talk about pi-Base/mathlib stuff: https://github.com/orgs/pi-base/discussions/627

[Josha Dekker]

Thank you for your kind invites! Yes, these files are in my repo, I’ll provide a bit context and where to find it tomorrow! (I didn’t document anything accurately I think, so I’ll make sure it is clear)

[Steven Clontz]

okay so I've figured out how to quantify over all compact Hausdorff spaces, and now I need to construct a specific one (the disjoint union of two converging sequences). Before I figure out how to construct this myself, is there any chance it is already in mathlib, or (more likely?) I can grab a copy of a converging sequence and a two-point discrete space and take their product?

[Steven Clontz]

oh I guess I could just use a subset of the reals :shrug: any hints on examples of such constructions is appreciated for thew newbie :upside_down:

[Jireh Loreaux]

How about OnePoint ℕ ⊕ OnePoint ℕ?

[Jireh Loreaux]

You'll probably have a little bit of work to do to massage things into exactly the form you want, but I would expect the lemmas you prove to be potentially usable elsewhere.

[Josha Dekker]

Let me start by saying that this project was/is very much work in progress. My goal was to automatically check what definitions/theorems from Pi-Base had already been formalised in Mathlib, to provide a nice to-do list for people interested in learning Lean. 

As a proof-of-concept, I wrote some code that automatically tried to find the associated Mathlib name lean_checklist_properties/properties_in_lean.lean for each property in pi-base. It then runs #check on each name, to see if it has already been declared. This is performed by scripts_for_progress/properties_to_cleaned.jl, which reads in the contents of properties. Of course, there are obviously quite some false negatives here, of which I tried to remove some manually by hard-coding them in said Julia file. 

Then, I translated each theorem in pi-base to a theorem in Lean format, which happens in two stages: theorems_to_cleaned.jl cleans up the theorem statements a bit, theorems_to_lean.jl then converts these to Lean statements, splitting them over a few files to avoid that the file becomes too slow. It then simply tries to prove every example by exact?, where any problem (missing definition/exact? failing) indicates that the theorem may not yet be in Mathlib. Of course, sometimes Lean would need a bit more help, so again expect some false negatives here. The translated theorems are in the lean_checklist_otherfolder.

Where my approach is different from what I've seen on your repo is that I didn't place new defs or theorems, but instead use #check and example … := by exact?. Together with the fact that I rewrote everything in terms of Mathlib names, this may make my files a bit unwieldy for your purposes, but feel free to use whatever you find in the repo!

I figured that a proper workflow should be fully dependent on Lean (rather than auxiliary Julia files) or the lean-formatting should be done at the pi-base side for long-run durability, so I decided to learn more functional programming and meta-programming in Lean to properly try to set this up, but a combination of steep learning curve and scarce time have prevented me from accomplishing this. 

If you are planning to include Lean declarations in pi-base, I think that is a better route, so I think that I will shift my attention to other projects. (Either way, it will take quite a while before I’m at the meta-programming skill level to continue properly on this project).

[Josha Dekker]

All in all, I really want to stress that what I've done is not rocket science/complete in any way, so please approach the problem in the way that you see fit. I'm more than happy to jump on a Zoom call sometime, although we should coordinate a bit: I'm based in Amsterdam (Netherlands).

[Josha Dekker]

I'm also more than happy to contribute if time allows! However, I unfortunately won't be able to join for both Zoom-meetings that you mentioned.

[Josha Dekker]

Also, see here for the Lean code @Eric Wieser used for the Matrix Cookbook. (That thread might also be of independent interest).

[Steven Clontz]

Jireh Loreaux said:

You'll probably have a little bit of work to do to massage things into exactly the form you want, but I would expect the lemmas you prove to be potentially usable elsewhere.

Thanks - I took a swing and missed in my latest PR commit to figure out how to define πBase.S20 [link] to be OnePoint ℕ, then use it in a theorem to show that all $k_2$-Hausdorff spaces are US (T425). Hand-holding is accepted if you have the hand to offer, but I also plan to dig around mathlib myself a bit more to puzzle out what I'm doing wrong.

I don't know what the review workflow is for mathlib (I see lots of open PRs!), but I look forward to figuring out one way or another how to best leverage the formalized results we model in pi-Base to grow mathlib's general topology content.

[Jireh Loreaux]

@Steven Clontz which PR?

[Andrew Yang]

#12387

[Steven Clontz]

Thanks @Josha Dekker for those details. I co-organized a workshop on math research cyberinfrastructure at the American Institute of Mathematics a few months ago, and pi-Base's founder @James Dabbs hacked out a somewhat similar proof of concept to point things on our side from pi-Base to mathlib: https://github.com/pi-base/data/pull/478 Demo: https://aim.topology.pages.dev/properties/P000001 (He has a days-old kiddo and has more important things than help me with this project at the moment.

As you say, I think adding lean identifiers to what we track at pi-Base is something we're interested and would help with wiring everything together. I'm too new to mathlib to know how interested this community would be in back-referencing pi-Base. But I agree that there's a lot of fun work to be done in Lean that would be well-motivated by the right connection between the pi-Base and mathlib.

Your project seems like it will, at the very least, be helpful for me to learn where pi-Base concepts are already modeled in mathlib. So thank you! And let's stay in touch. (If you'd like to become involved in pi-Base directly, I can suggest moving our community meetings to American mornings so more European folks can join in.)

[Jireh Loreaux]

#12387 is from a fork :sad:

[Steven Clontz]

I don't have write permissions for mathlib, or I'd be happy to make a branch on the core repo and make a new PR (assuming that's the preferred workflow)

[Jireh Loreaux]

For now it is. Give me a minute.

[Steven Clontz]

<- guy who didn't read https://github.com/leanprover-community/mathlib4?tab=readme-ov-file#contributing obvs

[Jireh Loreaux]

Invite sent: https://github.com/leanprover-community/mathlib4/invitations

[Jireh Loreaux]

I need to be done with Lean for the day, but I'll come back and take a look at this tomorrow.

[Eric Wieser]

It's not clear to me that mathlib is the right place for this pi-base tracking; I think it makes more sense to work on this in a separate repo (which could certainly live under leanprover-community if desired, or under the pi-base org!)

[Steven Clontz]

So I'm having fun hacking away at https://github.com/leanprover-community/mathlib4/pull/12436 but I think it's becoming clear that I might benefit from working on something that I could contribute to mathlib proper, and put my eyes on more Lean written by experienced folks that's been merged to mathlib. Any clues on where I might dig in?

[Steven Clontz]

Hm, on the topic of separation axioms, I see there's no non-Hausdorff completely normal property in mathlib. Would untangling those details be useful?

[Josha Dekker]

Steven Clontz said:

So I'm having fun hacking away at https://github.com/leanprover-community/mathlib4/pull/12436 but I think it's becoming clear that I might benefit from working on something that I could contribute to mathlib proper, and put my eyes on more Lean written by experienced folks that's been merged to mathlib. Any clues on where I might dig in?

What I did when I started a few months back was first identify pi-base stuff that was missing for which a similar concept had been formalized, and start writing api for that. For example: compact spaces had been done, so I formalized Lindelöf spaces. Now these have been merged, I’m PR’ing k-Lindelöf spaces in two PR’s. By this approach, you can benefit from learning the style used in existent files!

[Josha Dekker]

These are #11800 and #12087 by the way!

[Steven Clontz]

Cool. I did end up opening https://github.com/leanprover-community/mathlib4/pull/12458 to disintangle the T5 and completely normal properties. Could definitely use feedback as I know my proofs could be improved.

[Kevin Buzzard]

You are more likely to get feedback once you get #12458 onto the #queue, which means turning the red x which is currently on your PR into a green tick. At the bottom of the PR it says "some checks were not successful", and there seem to be two issues:

1) it seems that one of your proofs is unnecessarily verbose and a computer spotted this.
2) The file Counterexamples/SorgenfreyLine.lean no longer compiles and it's your job to fix this.

(I figured this out by clicking on various red x's around that part of the PR on the github page)

Feel free to ask questions if you can't get the green tick on the PR. If you manage to spot it on the queue then you've done what is necessary.

[Richard Osborn]

One tip is to put #lint at the bottom of the file you are working on (and delete it once you are done).

[Steven Clontz]

Thanks - I marked it as ready to view before I allowed CI to complete. I'll use those hints to get everything in order.

[Steven Clontz]

I think #12458 is now ready for review and I see it in #queue. I appreciate any other necessary pointers for my first contribution (and greatly appreciate all the feedback I've already received).