Errors: creating a project with Mathlib and SphereEversion

Stream: new members

[Sam Lindauer]

Hey all, I have a question on the creation of a project which depends on both the mathlib library and the sphere-eversion project. In the lakefile.lean file, I have added that the project requires these two git repos as follows:

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"
require SphereEversion from git "https://github.com/leanprover-community/sphere-eversion"@"master"

Both packages seem to have made it correctly into my .lake/packages folder. However, when I try to import them and restart the server, I get some different errors that make me believe that my Mathlib version might be a version ahead of the sphere-eversion project, although I am not sure if that is indeed the issue.

Some of the errors are:

• It imports Mathlib.Analysis.NormedSpace.AddTorsorBases instead of Mathlib.Analysis.Normed.Affine.AddTorsorBases
• failed rewrite in SphereEversion.ToMathlib.Analysis.Calculus.AffineMap.lean in the mapsTo_homothety_ball.
• failed use of nice_atlas_domain in stdLocalisationData in SphereEversion.Global.LocalisationData.lean
  And a selection of type issues.

My plan was to use this combination of libraries to work on a differential topology project within lean. Since I am quite new with lean and its ways, I am not sure if this is a known problem, if I am just being a little stupid or if it is just a case of fixing the errors locally to get it working. Either way, I hope someone has a possible answer. If any more information is needed, don't hesitate to ask.

Thanks, Sam

[Michael Rothgang]

Indeed, mathlib's master branch and sphere-eversion's master branch use different Lean versions. (Check the lean-toolchain file to determine which version is used.)

[Michael Rothgang]

I have an in-progress branch upgrading sphere eversion to current mathlib (but won't have time this week to finish it).

[Michael Rothgang]

That said: sphere eversion already imports mathlib - so if I understood correctly, you just need to require sphere-eversion (and not mathlib). In other words, I presume the correct fix is to not require mathlib.
@Jon Eugster I know you know about lakefile details: can you confirms this (don't require transitive dependencies) is correct?

[Michael Rothgang]

Taking a step back: it's great to hear that you want to work on differential topology! What particular goal would you work towards?

[Eric Wieser]

this (don't require transitive dependencies) is correct?

Yes

[Sam Lindauer]

Removing Mathlib from the requirements indeed works! Thanks so much!

[Sam Lindauer]

I have just started my master thesis and am currently getting familiar with how Lean works (I have worked through a couple of chapters in mathematics_in_lean). I am not yet completely clear on the formalization goal of the thesis as a whole yet, but as a start for now, the goal is to try to formalize the Whitney-Graustein Theorem in a stand-alone project.

[Jon Eugster]

Indeed, lake might get confused with transitive deps.

You can add the transitive dependencies to the lakefile but then you have to be super careful to use the right versions. Sphere eversion seems to use a random version of Mathlib at commit 2df7d9 (see it's lake-manifest) which isn't even a stable release, but somewhere a day after the v4.10.0 release of mathlib...

So I think the following would work too:

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"2df7d9446f22706562263d8b55076dc073e10d02"
require SphereEversion from git "https://github.com/leanprover-community/sphere-eversion"@"master"

but as said, it's superfluous to include the require mathlib and doomed to break the next time anything gets updated.

@Michael Rothgang I think you could add a rev to the sphere eversion's lakefile.toml then at least it would use one of the tagged releases of mathlib:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.11.0"

I think ideally almost all projects requiring mathlib as a dependency would not use "master" but any tagged release of mathlib, making it easier to combine different projects.

[Sam Lindauer]

That makes sense, thanks!

[Michael Rothgang]

Sure, adding a revision to sphere-eversion's lakefile is a good idea. I'll do so when I have time (not before next week).

[Michael Rothgang]

Do you have an eventual goal with your project? Just enjoy a fun master's thesis, formalise a new result, contribute something to mathlib? (To be clear: all three are fine!)

I vaguely remember a student (of @Patrick Massot @Floris van Doorn?) working in a similar direction as the Whitney-Graustein theorem. (Can you confirm, or am I misremembering?) In case your goal were "contribute to mathlib", it would be useful to take note of previous formalisations. (These might well be not at mathlib level yet - so this is not an argument to not work on this result. But it could be useful to see if they learned certain things on the way.)

[Patrick Massot]

I can confirm the intended fix to your lakefile issue is to require only the sphere eversion repository and not Mathlib.

[Patrick Massot]

I also confirm that Whitney-Graustein is a nice target. One important thing to understand is there are two completely separate tasks. One is to prove the h-principle for circle immersions into the plane. You can either deduce it from the sphere eversion project (which proves a much more general result) or write an elementary proof. The elementary proof from Making waves was the topic of a student project at CMU last year but was never completed.

[Patrick Massot]

The second independent task is to understand the homotopy obstruction. This is essentially equivalent to computing the fundamental group of the circle. I lost track of the status of this computation in Mathlib. Covering space theory and fundamental groups is a somewhat cursed area of Mathlib. Periodically someone announces they will work on it, some work is done but never PRed, or it is PRed but the process stops in the middle. There is no deep reason what this should stay that way however. You can be the one breaking the curse (after carefully checking the current status).

[Sam Lindauer]

@Michael Rothgang I think the eventual goal is to work on some new results in much less generality than what Mathlib asks. We have a few possibilities in mind: building on top of the assumption that differential forms exist and try to work on Symplectic or Contact manifolds, having a look at the formalisation of differential forms themselves and looking at the formalisation of the holonomic approx. thm for 1-jets provided by @Patrick Massot and Mélanie Theillière. We haven't chosen a specific path yet though.

I will be working under supervision of Johan Commelin and Álvaro del pino Gomez.

[Patrick Massot]

I don’t think the current state of Mathlib allows to work on differential form, unless Yury really prioritizes this (he seemed to have resumed work on it).

[Johan Commelin]

One option we considered is to hand-roll differential forms in a rather specific setting of smooth manifolds over $\R$. So no worrying about other fields or structure groupoids, etc...

[Johan Commelin]

This wouldn't end up in mathlib, but it might still give some input for how a mathlib formalization should proceed.

[Patrick Massot]

Why do you think this would make things simpler?

[Johan Commelin]

because I don't know what the correct conditions on a general structure groupoid are to get a sensible theory of differential forms

[Johan Commelin]

but I do know that differential forms are sometimes considered on manifolds with boundaries etc...

[Michael Rothgang]

I haven't thought about differential forms yet (and am not sure if I can commit time to it) - but let me say I would be excited to see (or review) work towards symplectic geometry!