Toward a new formalization of real numbers