Status of field theory in Mathlib 4

Stream: mathlib4

[Cody Roux]

I'm kind of curious about the level of effort required to prove that the theory of algebraically closed fields of fixed characteristic is categorical at a given cardinal.

It looks like a couple of lemmas needed are:

• An algebraically closed field of cardinality k has a transcendence base of size k
• Two fields of the same char with the same cardinality transcendence base are isomorphic

I hope I got those right.

How close are we to proving those theorems in the current ecosystem?

[Ruben Van de Velde]

Are the things in https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/IsAlgClosed/Classification.html relevant?

[Cody Roux]

Oh yeah! What do you know. Wow it feels very accessible to prove completeness of closed fields!

[Ruben Van de Velde]

I would generally suggest clicking on "Imported by" on the right hand side of that page to see if anything within Mathlib builds on top of these results, but in this case there's nothing

[Cody Roux]

For note: These theorems, combined with Łoś–Vaught https://leanprover-community.github.io/mathlib4_docs/Mathlib/ModelTheory/Satisfiability.html#Cardinal.Categorical.isComplete brings completeness of complete fields within striking distance

[Cody Roux]

Sadly completeness only implies decidability on paper; the algorithm is completely impractical

[Cody Roux]

But it has cool applications! E.g. a proof of Ax-Grothendieck uses this.

[Alex J. Best]

You might be interested in https://github.com/Jlh18/ModelTheory8Report/blob/main/report/m4r.pdf (its in lean 3 but still cool!)

[Cody Roux]

Wow the whole thing is already done! I'm constantly amazed at the maturity of the lib. A tiny bit sad this hasn't been ported yet.

I guess the very last step would be trying to make this a "tactic" that reduces a proposition over

$$\mathbb{C}$$

to

$$\exists n, \forall p > n, \overline{\mathbb{F}}_p \ \ldots$$

has anyone done that?

[Johan Commelin]

I'm not aware of that.

[Kevin Buzzard]

Cody the Ax-Grothendieck thing above was just a masters project I supervised. I don't think anyone is trying to port it right now and I can't claim that it was done in the best way because the supervisor knew very little about what was going on in that project.

[Michael Rothgang]

Is #6468 a port to Lean 4? (Many pieces of it were merged, but as far as I can see, the remainders are available for somebody to pick up and finish.)

[Kevin Buzzard]

Looks like it! Certainly Chris (the author of the PR) helped a lot with the project

[Chris Hughes]

Cody Roux said:

Wow the whole thing is already done! I'm constantly amazed at the maturity of the lib. A tiny bit sad this hasn't been ported yet.

I guess the very last step would be trying to make this a "tactic" that reduces a proposition over

$$\mathbb{C}$$

to

$$\exists n, \forall p > n, \overline{\mathbb{F}}_p \ \ldots$$

has anyone done that?

I'm a little bit late here, but I would argue that this tactic is not the main thing that you need.

Most example of first order properties are infinite collections of formulas, or formulas that themselves depend on some Lean variables. For example the Ax-Grothendieck theorem has to be split into an infinite collection of formulas, one for each set of monomials in the polynomial map.

Another application I've seen of this is that for any finite semigroup $G$, the statement $G$ has a faithful representation of dimension $n$ is a first order formula. Another example is the fact that adjoining a square root of -1 to a real closed field gives an algebraically closed field (I think this would be one formula for each $n$ to say that every polynomial of degree $n$ had a root, as well as some work to prove that evaluating a polynomial over the extension was definable as a function on pairs of elements of the base field).

I think the main thing required here is just a library with a lot of different ways of constructing these formulas. (I think this is the answer to a lot of questions. Where people think automation is needed, a bigger library would often work instead). For example, for the fact about semigroups above you will need to know that matrix multiplication is a definable function. You also need constructors for quantifying over an arbitrary finite set of variables docs#FirstOrder.Language.Formula.iAlls, and definitions for proving that properties of definable functions like injectivity are first order and so on mathlib4#20180

[Cody Roux]

Maybe we just need a really (really!) complete library. But this does seem like a departure from informal maths, where one says "oh and just look at our informal development, you can observe that everything is first order". Now instead we need to build all these observations in by hand. Maybe it's the computer scientist in me, but some of this has to be automatable, no?

Otherwise it feels like we're just building a theorem prover "one floor down".

[Adam Topaz]

I would love to have some tactic (or more general meta code) that transports terms across some isomorphism of structures (in the sense of model theory).

[Adam Topaz]

And perhaps a los tactic that lets you prove a first order goal about an ultraproduct by proving it on a large set of the factors

[Patrick Massot]

@Reid Barton probably has useful comments here (coming from his work on o-minimality).

[Cody Roux]

That would be nice, though I personally feel like people use ultraproducts when they could use completeness. Maybe the former avoids this problem of "syntactification"

[Chris Hughes]

I think it's likely that mathlib would handle ultraproducts better than the syntactic approach, simply because the library has been set up to deal with isomorphisms and products and so forth of algebraic structures already, so lemmas about how matrices behave acros homomorphisms are already there, but the corresponding infrastructure isn't there in a model-theoretic way. I don't have a stance on which is better out of syntactic or ultraproducts, probably the best one is whichever is more familiar to the user and mathlib should aim to support both.

[Chris Hughes]

Cody Roux said:

Maybe we just need a really (really!) complete library. But this does seem like a departure from informal maths, where one says "oh and just look at our informal development, you can observe that everything is first order". Now instead we need to build all these observations in by hand. Maybe it's the computer scientist in me, but some of this has to be automatable, no?

Otherwise it feels like we're just building a theorem prover "one floor down".

I think the closest practical approach to this is to have really nice notation for writing down formulas, but the user would still be writing a Formula, and not a Lean term with a tactic to reverse engineer the FirstOrder Formula whose semantics are the Lean term. simp is very good at proving that formulas have the expected semantics once you've written down the formula. (Incidentally I'd love to have nice notation like this in other areas of mathlib as well, for example it would be great to use lambda calculus to write down morphisms in a Cartesian closed category).

I do think there's an awful lot of things that feel automatable in mathlib but aren't automated. Every time you define a new algebraic object there's a long list of simp lemmas to prove that feel very repetitive but the practice seems to say that they're not quite repetitive enough to be able to automate yet. But maybe we haven't tried hard enough.

[Cody Roux]

Hmmm, maybe this is a good opportunity for a macro dsl, whatever they're called.