David Kurniadi Angdinata: Division polynomials of elliptic c

Stream: Lean Together 2025

[Henrik Böving]

@David Ang https://github.com/leanprover/lean4/pull/6679

[David Ang]

Thanks! Here are my slides.

[Riccardo Brasca]

@David Ang how can implementations of the schoof algorithm work in practice if the formulas of the division polynomials are wrong?

[David Ang]

In general, I don't know. I know that many people only care about the short Weierstrass equation with a1 = a3 = 0, so the formula for omega is fine. I know that Sage doesn't have a formula for omega but does something similar by "consideration of the invariant differential"

[Riccardo Brasca]

I mean, the algorithm absolutely depends on the explicit formula, and in practice it works (it agrees with other algorithms). Maybe it is a char 2 thing?

[Riccardo Brasca]

I mean, is the literature correct with the short equation?

[David Ang]

Yes, it is correct with the short equation

[David Ang]

Char 2 has been haunting me since the associativity days :upside_down:

[Riccardo Brasca]

Ok so I think the implementations only use the correct cases (to know if the number of points is even there is no need to use the division polynomial)