@tao Out of curiosity, how difficult are such interval arithmetic calculations? I'm curious how far one is from a Lean version of Abramowitz and Stegun.