Since we know that these hyper real numbers are well defined we can teach them axiomatically to high school students the way Leibniz used them (and keep the exp

Since we know that these hyper real numbers are well defined we can teach them axiomatically to high school students the way Leibniz used them (and keep the explicit construction via filters to university students just like with a dedekind cut for reals) Here is the axiomatic approach in Julia and Lean https://github.com/pannous/hyper-lean https://github.com/pannous/hyper-lean