Zulip Chat Archive
Stream: Lean Together 2026
Topic: Vasilii Nesterov - Verified computation of real asymptotics
Jireh Loreaux (Jan 19 2026 at 14:52):
Discussion thread for the talk.
Thomas Browning (Jan 19 2026 at 15:01):
Seems like adding multiseries requires comparing the real-valued exponents. Does anyone know how this is being done?
Jireh Loreaux (Jan 19 2026 at 15:22):
There is an open PR for this work, see #28291
Vasilii Nesterov (Jan 19 2026 at 18:45):
Thomas Browning said:
Seems like adding multiseries requires comparing the real-valued exponents. Does anyone know how this is being done?
Yes, the tactic uses a "zero oracle," which is an arbitrary meta-program that takes an expression x representing a real number and returns a proof of x ? 0, where ? may be =, <, or >. Currently, I use a combination of the simp, norm_num, linarith, and positivity tactics, but this part of the tactic is completely modular, so it can be replaced with something else (I'm thinking about trying new interval arithmetic tactics here). You can see the actual code here.
If the zero oracle fails, then compute_asympotics also fails with a message like "cannot compare x with zero, please add a have statement before the compute_asympotics call".
Vasilii Nesterov (Jan 19 2026 at 18:53):
Slides: LT_2026_compute_asymptotics.pdf
Snir Broshi (Jan 19 2026 at 19:50):
Vasilii Nesterov said:
x ? 0, where?may be=,<, or>
C++/PHP/Perl use the notation x <=> 0, the Spaceship operator :flying_saucer:
Nick Adfor (Jan 20 2026 at 07:30):
Last updated: Feb 28 2026 at 14:05 UTC