Neron models in Lean

Stream: new members

[David Holmes]

Hi all,
Tentatively thinking about getting some local people together to try to simultaneously learn Lean and formalise something fun. Wondering if Neron models might be a suitable topic? I'm thinking of Neron models of abelian schemes over generic points of DVRs (maybe with perfect residue fields).
I seem to remember that schemes have been formalised, if the notion of smooth morphism has also been formalised then that's most of what one needs for the definition, though I can imagine setting this up correctly will already be work. To prove existence one needs blowups, no idea if anything has been done about this.

It could be that this has already been done, or that it's vastly too ambitious. Or that I should do my homework properly before posting here - either way, please let me know!

[Andrew Yang]

Hello! We are definitely able to write down a definition, and it might be a fun exercise to write it down. But to prove anything about it might need substantial more work.

[Kevin Buzzard]

Jacobians might also be an interesting target

[Bartosz Naskręcki]

I am interested in implementing regular models, following Tim's code (https://people.maths.bris.ac.uk/~matyd/newton/). I am using Aristotle from Harmonic and the lack of such things have been an obstructio for my work.

[David Holmes]

@Andrew Yang Happy to hear writing out a definition might be a reasonable exercise. I guess there are various basic checks one can then think about (uniqueness, descent, separatedness, quasi-compactness...), and see how things are going before deciding whether to try to actually prove the general existence result.
@Kevin Buzzard Jacobians sound fun, cut I have a vague impression that things involving any significant amount of category theory tend to be painful in Lean? I guess in any case one should start with Hilb or Quot (unless one wants to go via Artin's axioms and algebraic spaces, but I'd guess that would be harder?)
@Bartosz Naskręcki Sounds as if you are proposing proving resolution of singularities for arithmetic surfaces? Naively I'd guess that is hard...

[Filippo A. E. Nuccio]

Bartosz Naskręcki said:

I am interested in implementing regular models, following Tim's code (https://people.maths.bris.ac.uk/~matyd/newton/). I am using Aristotle from Harmonic and the lack of such things have been an obstructio for my work.

Just out of curiosity, have you been exposed to a regular Lean course, or have you tried to formalize things on your own, or do you only rely on Aristotle? And when you speak about "your work" do you mean "your formalisation work" or something else?

[Bartosz Naskręcki]

Filippo A. E. Nuccio said:

Bartosz Naskręcki said:

I am interested in implementing regular models, following Tim's code (https://people.maths.bris.ac.uk/~matyd/newton/). I am using Aristotle from Harmonic and the lack of such things have been an obstructio for my work.

Just out of curiosity, have you been exposed to a regular Lean course, or have you tried to formalize things on your own, or do you only rely on Aristotle? And when you speak about "your work" do you mean "your formalisation work" or something else?

I was and I have worked on some small projects in Lean just for myself. But now with the advent of auto-formalization engines I see that one of the very hard obstructions to practically use them in one's particular idea is the lack of formalization of very simple concepts. Aristotle when asked to compute Kodaira type for an elliptic curve is really trying to invent Tate algorithm from scratch. This is super inefficient and makes the output code sometimes work but horribly inefficient.

[Kevin Buzzard]

In my mind a huge impending bottleneck in getting formalization to be a part of AI doing mathematics is the fact that there is an extremely long list of missing but actively-used-in-modern-research definitions in mathlib (which is streets ahead of the other maths libraries in most areas of modern research, so it's basically equivalent to claim that there's a long list of missing definitions in the union of all formalized libraries). We accelerated fast through undergraduate mathematics because although it needed some thought there was still a broad base of people who could formalize it. But the number of Lean experts who could formalize Tate's algorithm is -- what -- at most 20 people? And these people are typically professors busy teaching courses and not being rewarded for their formalization work, or PhD students working hard on other projects etc. As the work on AI solving Erdos problems recently indicates -- "if you build it, they will come". But we have to build it. And without it we run the risk of unverified AI slop becoming the norm.