Issues

• Axiom census: Lean.collectAxioms under-reports axioms of imported inductives on v4.30.0 and later (lean4#15226)

  daira/CompElliptic#39 · Filter by author daira opened on Nov 9, 2026

• Compressed Pasta point decoding (fromBytes), the inverse of toBytes

  daira/CompElliptic#38 · Filter by author daira opened on Nov 7, 2026

• README: the "Present so far" status list is stale

  documentation
  daira/CompElliptic#34 · Filter by author daira opened on Sep 8, 2026

• Function-field vocabulary and Riemann's inequality: a formal genus bound for the Weil input

  daira/CompElliptic#30 · Filter by author daira opened on Aug 18, 2026
  1

• Check the SSWU implementation directly against Rust pasta_curves

  enhancement
  daira/CompElliptic#24 · Filter by author daira opened on Aug 11, 2026

• Gate the FastFieldNative precompile lane behind a config option

  daira/CompElliptic#18 · Filter by author mitschabaude-bot opened on Jul 28, 2026

• Reconcile the fast projective arithmetic with the CoordinateSystem abstraction

  enhancement
  daira/CompElliptic#15 · Filter by author daira opened on Jul 27, 2026

• Dedicated proven doubling for the fast projective ladder

  enhancement
  daira/CompElliptic#14 · Filter by author daira opened on Jul 27, 2026