Unknown identifier ?

Stream: general

[Sophie Morel]

Okay, I hope that the explanation for this is that I am very stupid, but I am very confused: I am getting an 'unknown identifier' error for a lemma that is in mathlib. I did import the relevant file, I am in a working Lean project, and I checked some lemmas from the same file - they work ! I tried copy-pasting the name of the lemma from the mathlib page because I thought I might have made a typo, it made no difference. Here is a MWE:

import data.set.basic

#check set.ssubset_iff_insert  -- that one is fine...

#check set.subset_insert_iff_of_not_mem  --unknown identifier 'set.subset_insert_iff_of_not_mem'

Here is the mathlib link: https://leanprover-community.github.io/mathlib_docs/data/set/basic.html#set.subset_insert_iff_of_not_mem
The lemma that checks on the previous line is the next lemma in data.set.basic. I admit that I am totally mystified... :-(

[Yaël Dillies]

It works for me. What's your mathlib version? Probably it is outdated and you do not in fact have set.subset_insert_iff_of_not_mem in your local copy of mathlib.

[Sophie Morel]

How do I find out what my mathlib version is ?

[Sophie Morel]

I forgot to say that I ran 'leanproject get-mathlib-cache' before posting, but maybe that is not sufficient.

[Yaël Dillies]

https://mathlib-changelog.org/theorem/set.subset_insert_iff_of_not_mem says that lemma was added fairly recently. Odds are you downloaded mathlib before the 22nd of February.

[Yaël Dillies]

Are you working on the mathlib repository or on a separate project (in the sense of leanproject)?

[Sophie Morel]

A separate project. Do I just need to run 'leanproject upgrade-mathlib' ?

[Yaël Dillies]

Yes. I personally do leanproject up, which should be a synonym of leanproject upgrade-mathlib.

[Sophie Morel]

Well, I launched the command, let's see what happens.

[Sophie Morel]

I'm bookmarking that changelog page, it's very useful.

[Yaël Dillies]

Sophie Morel said:

How do I find out what my mathlib version is ?

The answer to this question is "Go to leanpkg.toml". The one from LeanCamCombi is

[package]
name = "lean-cam-combi"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "dc65937e7a0fff4677f0f5a7086f42da70a69575"}

This means that LeanCamCombi uses version 3.50.3 of the community version of Lean, and version dc65937e7a0fff4677f0f5a7086f42da70a69575 (this is actually a commit identifier) of mathlib.

[Sophie Morel]

Yup, now it works ! Whew, I'm so relieved that it was me doing something stupid and not a horrible bug in my mathlib installation. (Also, I now know how to update. Somehow I thought that 'leanproject get-mathlib-cache' was enough. I'm not sure.) Thank you very much !

[Yaël Dillies]

leanproject get-mathlib-cache (aka leanproject get-m) downloads the cache for the version of mathlib you're on, but it does not change the version itself.

[Yaël Dillies]

If you're working alone on that project, then you should never need leanproject get-m because leanproject up runs it for you (but if a collaborator runs leanproject up, or just you from another machine, then you'll need to run leanproject get-m once you pull their changes).

[Sophie Morel]

I'm working alone on this particular project, but I just started another project with a group of people, so that last piece of information will definitely be useful.

[Sophie Morel]

By the way part of my project is based on your mathlib file on simplicial complexes. I actually needed abstract simplicial complexes, but I reused some of the basic structure of the file, as I have almost no experience with setting up Lean definitions and having a model was very helpful. So I'm really glad that it was there !

[Yaël Dillies]

Oh great! In fact, @Shing Tak Lam already "abstracted" my simplicial complex files on branch#shing-asc, if you want to compare. And did you know I have a lot more simplicial complex material on branch#sperner-again?

[Sophie Morel]

No, I don't know about anything not in mathlib. I'll check out these branches. My main focus was shellability and the calculation of the Euler-Poincaré characteristic of a finite shellable complex.

[Yaël Dillies]

If you need this material, I can move it to mathlib, but I would rather do it after the port because it's mostly unpolished. I also have a definition of the Euler characteristic in the generality of incidence algebras in #11656 with Alex J. Best, although there's some work to be done to connect it to concrete examples.

[Sophie Morel]

Well, I proved everything I needed about abstract simplicial complexes and I have moved on to the applications I had in mind (showing that a certain poset is isomorphic to the face poset of a shellable abstract simplicial complex and using that to calculate some alternating sums on the poset). So there's no rush.

[Sophie Morel]

Interesting, Shing Tak Lam seems to have an essentially equivalent but much better (in Lean) definition of dimension, but we have a different definition of "pure".

[Yaël Dillies]

Although we're both third year Cambridge undergraduates, Shing had way more experience when he wrote that code than when I wrote mine which inspired his. Sperner's lemma was basically my first project!

[Sophie Morel]

Cool ! I decided to try and formalize my simplest paper as my first project. Turns out it was less simple than I thought. (Because importing non-formalized results is cheating, so I have to formalize the prerequisites too.)

[Yaël Dillies]

Formalising a paper, however simple it is, is no simple task!

[Sophie Morel]

Well, whew, I am done ! (It's only the first half of the paper, but that's what I had set out to do anyway.) I thought that it would take a couple of weeks and it took two months, which is about par for the course whenever I set out to write a maths result.
Next steps: (1) clean the code and (2) translate it into Lean4 (I think that all the prerequisites are already ported - famous last words, I know, I know), probably at the same time.
@Yaël Dillies , would it be okay if I use yours and @Shing Tak Lam 's code as inspiration for step (1) ? I would give credit where credit is due, of course.

[Yaël Dillies]

Absolutely no problem! I wouldn't be working on mathlib if I didn't want my code to be reused :wink:

[Yaël Dillies]

And this is great news! I'm excited to see the result.

[Sophie Morel]

Thanks ! Oh yeah, I forgot goal number 3: learn to write a fancy website like that of the sphere eversion project. That should only take 5 years... :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

Modulo the initial set-up (which people here can help with), making the fancy website is little more than writing the TeX code and then letting the machines do their work.

[Kevin Buzzard]

@Sophie Morel congratulations! Which paper of yours have you half-formalised?

[Sophie Morel]

Sections 1-4 of this:
https://alco.centre-mersenne.org/item/10.5802/alco.66.pdf
Including all the prerequisites about abstract simplicial complexes. There is no "sorry" anywhere in the files and they all build, but I had to increase the timeout and memory limits quite a lot. And okay, to be honest I didn't formalize the stuff about geometric realizations; it's probably not as hard as I imagined at first, and I can sort of see how it would go, but it would require a lot of additional time.
I had to doubt that the results were correct, but I wanted to see how hard it would be to convince Lean of that. In fact I spent most of the time on the background material, so I guess that this kind of thing will become easier as mathlib grows, but there will still need to be some progress before we can convince more people to attempt it.

[Sophie Morel]

Now that I think about it, this particular paper is supposed to give a "better" (as in "more natural") proof of a bunch of combinatorial identities that I had encountered while calculating the cohomology of Siegel modular varieties, and if which I was much less certain, before we managed to reprove them in a geometric way.In fact, I'm still not sure that the original proof is 100% correct. Formalising that original proof would probably have been much easier - no background required, it was all brute force inductions - and it would have made me feel better about them at the time. On the other hand, looking for a better proof was a lot of fun too. I'm not sure what the conclusion of all this is.

[Kevin Buzzard]

I just regard these sorts of projects as useful data points. If you want to formalise 8 pages of formalisable mathematics, how long does it take? Depends on lots of things. But right now we're getting it to "in many areas it's now possible for a small team to do this" which is good to see

[Sophie Morel]

@Kevin Buzzard Well here's another useful data point for you: one month later, I have a Lean4 version of my formalization project (starting from the Lean3 version and zero knowledge of Lean4):
https://github.com/smorel394/TS1
I also cleaned stuff up a lot between the two versions, though it's still far from perfect. I realized that some of the statements generalize, but I'm not sure in which direction I should take them; I need to learn more stuff about the infinite symmetric group.

[Pietro Monticone]

Congratulations @Sophie Morel and thank you for this insightful related talk!

[Johan Commelin]

I like it that Deligne asks at the end of the video whether Lean can do transport of structure. He knows exactly where the struggles are :smiley:

[Adam Topaz]

There’s an older video of a lecture by Deligne about motives I think where he talks about “transport of structure” in the context of the Galois action on ell-adic cohomology. I’m not surprised he asked that question :)

[Scott Morrison]

Jake Levinson and I have been thinking a bit about "transport of structure" again. We have some meta code, and a plan, but nothing to show off yet.

[Sophie Morel]

Oh dear, I was careful not to mention it to Kevin so it wouldn't end on his twitter feed, but I guess it's impossible to hide this kind of stuff now that everything is online.
I was annoyed that I spent too much time on introductory stuff and not enough on the project itself, but then I talked to people and they said they were happy I did that. Still, I think it should be possible to find a better balance.

[Sophie Morel]

Johan Commelin said:

I like it that Deligne asks at the end of the video whether Lean can do transport of structure. He knows exactly where the struggles are :smiley:

We actually continued that discussion after the talk was over and we were no longer being recorded. There was no definite conclusion apart from the fact that it's hard. (I was bitten by that very thing when I realized that I had proved shellability of a certain simplicial complex in Lean and wanted to apply it to a complex that was "obviously isomorphic" for a mathematician, but not so obviously for Lean. Also, I hadn't told Lean that shellability was transported along isomorphisms...)

[Johan Commelin]

Sophie Morel said:

I was annoyed that I spent too much time on introductory stuff and not enough on the project itself, but then I talked to people and they said they were happy I did that. Still, I think it should be possible to find a better balance.

Welcome to the experience of giving Lean talks for an advanced mathematical audience :rofl:

[Sophie Morel]

Also, not sure if anybody watched Björg Poonen's talk of the next day, but he made a Lean joke during it. I was a really nice moment.

[Johan Commelin]

I'll put it on my watch list

[Johan Commelin]

Here's a direct pointer into Bjorn's talk: https://www.youtube.com/watch?v=djYSWwgSeI4&t=1391s

[Ruben Van de Velde]

Seemingly well received by at least one person

[Adam Topaz]

Proof: sorry $\square$