Isaiah Mindich

Stream: new members

[Isaiah Mindich]

Hello,

I'm a PhD student at Rice University studying arithmetic geometry. I don't expect to be doing much formalization as part of my graduate research, but I am interested in making some contributions in my spare time. I am most of the way through the Mathematics in Lean book, and also have some experience with Coq and Haskell.

Has there been any work done on formalizing the Lindemann-Weierstrass theorem, either inside or outside of mathlib? The mathlib website claims that it has not been formalized yet. If it hasn't, I was considering formalizing the proof given in Jacobson's Basic Algebra I.

[Kevin Buzzard]

No this has not been done yet in Lean, although it was done in Coq a few years ago https://link.springer.com/chapter/10.1007/978-3-319-66107-0_5 and was also done in Isabelle/HOL very recently https://www.isa-afp.org/browser_info/current/AFP/Hermite_Lindemann/document.pdf .

If you are interested in arithmetic geometry, why not formalise some arithmetic geometry instead? Nothing has been done before in any theorem prover other than what we have (basic Hartshorne ch2 stuff)

[Kevin Buzzard]

On the other hand, we have all the prerequisites for L-W (multivariable polynomials, complex analysis) so it's certainly a feasible project.

[Isaiah Mindich]

That's a good point about arithmetic geometry. I was thinking of the Lindemann-Weierstrass theorem mostly because it is a fairly self contained result that, as you mentioned, does not depend on anything that hasn't been formalized yet. But I am also certainly interested in the ongoing effort to formalize scheme theory. My main concern is that my time is limited and I don't want to block somebody else's work.

[Kevin Buzzard]

Algebraic geometry is just worked on collaboratively by a bunch of people, this is an open source project and people just come and go, I don't get the impression that people can block other people's work.

[Eric Wieser]

The best way to avoid blocking people, while still having people use your work, is to try and split it into small pieces. That way if you disappear half way through, then half your work ends up in mathlib, rather than ending up with a single half-complete PR that gets abandoned.

[Isaiah Mindich]

In that case I'll take a look at the AG stuff in mathlib and see if there's anything I might want to work on. (I still might attempt L-W, as I'm trying to teach myself some transcendental number theory on the side)

[Kevin Buzzard]

yeah don't let me discourage you from L-W -- there is plenty to do all over the place and you should do what you think will be most fun :-)

[Isaiah Mindich]

Are the AG versions of dimension and codimension (and basic results about them) formalized? I see that there are very general definitions of Krull dimension, height, etc for preorders, but I didn't see any of that stuff applied to schemes. I also couldn't find anything in Topology, which is where other properties like Noetherianness are.

[Ruben Van de Velde]

Re L-W, this was mostly done in lean3: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lindemann-Weierstrass.20theorem.20almost.20done

[Johan Commelin]

cc @Isaiah Mindich :up:

[Ruben Van de Velde]

I'd be happy to port that work if that's helpful. I think there's a missing part about symmetric polynomials

[Isaiah Mindich]

Thanks, but I don't know much free time I'll have once the fall semester starts, so I would not recommend porting it unless you know someone has serious plans to finish it. I'm also still not sure if I want to work on that or something from AG/commutative algebra. It might be interesting to formalize some basic results about dimension (in the "chains of irreducible closed subsets" sense). There doesn't seem to be that much related to that in mathlib, and it would give me a chance to learn about how Lean deals with topological spaces.

[Ruben Van de Velde]

Well, I'd like it to end up in mathlib regardless of whether you'll work on it :)

[Jack J Garzella]

Isaiah Mindich said:

Are the AG versions of dimension and codimension (and basic results about them) formalized? I see that there are very general definitions of Krull dimension, height, etc for preorders, but I didn't see any of that stuff applied to schemes. I also couldn't find anything in Topology, which is where other properties like Noetherianness are.

@Calvin Lee and I are working on more specific definitions/theroems about height, dimension, and dimension theory, as well as other odds and ends in commutative algebra. We have this blueprint outlining what we're doing which is a little... disorganized right now, but there are certainly small-ish self-contained things that can be done, if you're interested don't hesitate to reach out to one of us.

[Kevin Buzzard]

@FMLJohn you might want to talk to these people about Krull dimension!