Article formalization

Stream: job postings

[Cody Johnson]

Hi, I'm offering $1000 for anyone who is able to help formalize the following article by November 30th (flexible): https://arxiv.org/abs/2012.12475 Please DM me if interested!

[Scott Morrison]

err... I'm glad you didn't specify November 30th in any particular year.

[Kevin Buzzard]

I should think that if someone were to get working on this now, then by the 30th they might have the definitions of c_4 and c_6 and N; for this we'd need to formalise the algorithm giving a global minimal model and Tate's algorithm for computing the conductor. That would get you into the second paragraph of page 1. To talk about the group of points of an elliptic curve one would have to prove associativity; the conceptual method for doing this via Picard groups took 6700 lines of code in Coq. The brute force method via bashing out the formulae would take fewer lines of code but there is a chance that ring will time out -- we never tried yet. Then things will get easier; the issue is that the foundations are not really there yet. The full proof of Theorem 2.2 is hundreds of pages long and relies on a bunch of hard algebraic geometry, so one would have to skip that. At first glance, the rest of the paper doesn't look too bad, but formalising takes time; I should think a more reasonable time frame would be a year rather than two weeks. The problem now is that if you have a year to formalise a random maths paper, why choose some random paper on ArXiv as opposed to something famous? In some sense the formalisation problem can be divided into two parts: firstly the project of getting the basics of the arithmetic of elliptic curves over the rationals (and more generally over global fields) up to speed (e.g. group law, conductor, global minimal models in class number 1 case), and then secondly the content of the paper. Both of these will take quite some time to do in practice.

[Kevin Buzzard]

If you just wait then the basics of the arithmetic of elliptic curves will happen organically (e.g. I have some students who will be working on Modell-Weil during the first half of 2022). Once the basics are there, formalising the paper becomes something which one can actually consider a reasonable project.

[Kevin Buzzard]

I think that Theorem 3.3 might actually assume Mazur's theorem, at least the way it's proved, which is going to be very problematic for a full formalisation.

[Yakov Pechersky]

What about stubbing out any dependent theorem as a sorry, and just getting the paper in a blueprint state?

[Cody Johnson]

Yeah, I agree it would be quite hard to formalize all of the required dependencies. Do you think if you could sorry out the dependent theorems it'll be doable?

[Kevin Buzzard]

The conductor of an elliptic curve over the rationals is quite a delicate invariant. One way of starting would be by sorrying the definition of conductor and of the group law (or, better, defining addition and then sorrying associativity); then I could imagine that one could proceed far more rapidly.

[Cody Johnson]

Yeah I'm totally fine with that.