LMFDB natively in Lean

Stream: maths

[Joachim Hauge]

There is a site http://www.lmfdb.org that describes some invariants of interesting number-theoretical objects. Have people considered defining all these things in Lean and formalizing the algorithms for computing the invariants?

[Patrick Massot]

I'm pretty sure Kevin considered formalizing the math part. But there are still missing dependencies.

[Kevin Buzzard]

We're slowly making all of those objects: number fields, elliptic curves, modular forms etc. By "formalizing an algorithm" do you mean just writing it in Lean (4?) or also proving that the algorithm works? My impression is that it's Coq which is the master of this stuff, it can do accurate numerical integration for example, which is important for Cremona's algorithm for computing elliptic curves from modular forms.

[Kevin Buzzard]

But I am not even sure that it is possible to formalise some of these algorithms, as they might assume the easy direction of modularity of elliptic curves -- every modular eigenform with integer coefficients gives rise to an elliptic curve with the same conductor. How are you going to prove that in Lean -- that's a way off. IIRC part of the algorithm is "oh we have some numbers A and B except they're random real numbers, but we know there is a real number r such that r^4A and r^6B are integers, oh look, this real number which we found from some fiddling about seems to work quite well, and now we compute the conductor of y^2=x^3+(r^4A)x+(r^6B) and oh great it's the level of the form, so we probably did it right"

[Alex J. Best]

In @Assia Mahboubi's habilitation (https://tel.archives-ouvertes.fr/tel-03107626) p.82 Assia talks about the potential project of verifying the modular forms data in the LMFDB (presumably in Coq but its certainly of interest here too!).