lean-inf Compute with infinities and infinitesimals! A calculator using the Levi-Civita field, implemented in Lean 4 as a datatype. Gives autodiff for free.