{"id":"palomar/PALOMAR-2026-10-28-000013","url":"https://github.com/manvirjaswal/z2z4-rank6-lean/tree/84d579ace25e4412c9df723c17a13cd4dec096e5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000013-v1.json","repo":"https://github.com/manvirjaswal/z2z4-rank6-lean","tags":["math.NT","msc:11G05","msc:14J27","msc:11G35"],"score":0,"title":"Infinitely many elliptic curves with torsion Z/2Z × Z/4Z and rank at least six","trust":"high","domain":"math.NT","source":"palomar","authors":["Manvir Jaswal"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 and Mathlib formalization of the paper \"Infinitely many elliptic curves with torsion Z/2Z × Z/4Z and rank at least six\" by Manvir Jaswal. Theorem 1.1 says that infinitely many elliptic curves over Q have torsion subgroup Z/2Z × Z/4Z and rank at least six, with infinitely many distinct j-invariants. The curves are fibers of a one-parameter family of Dujella and Peral, y² = x(x + a²)(x + b²), which has rank three over Q(m) and gains three further independent points over the function field of a curve C of genus one; congruences carry the independence of the six points, and the torsion,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Infinitely many elliptic curves with torsion Z/2Z × Z/4Z and rank at least six","identifier":"https://doi.org/10.5281/zenodo.23437117","relationship":"formalizes"}]}