エウドクソス
A relatively less known construction allows to define real numbers using only the additive group of integers formula_66 with different versions. The construction has been formally verified by the IsarMathLib project. Shenitzer and Arthan refer to this construction as the "Eudoxus reals", named after an ancient Greek astronomer and mathematician Eudoxus of Cnidus.