（関連ページ）
https://www.reddit.com/r/math/comments/1kcnu7l/are_cauchy_sequences_the_most_useful_ways_to/
質問 r/math
1年前
PhantomSasuke
Are Cauchy sequences the most useful ways to define Real numbers?
Proof assistants like lean define real numbers as equivalence classes of Cauchy sequences which allows it to formalise the various results in analysis and so on.
I was curious if alternate definitions (such as Dedekind cuts) of the real numbers could be used to streamline/reduce the complexity of formal proofs.
（回答(抜粋)）
Melchoir
1 年前
In the context of Lean, Kevin Buzzard started a thread asking a related question in 2019 here, then wrote some thoughts on the topic in 2020 here.
The current documentation for the standard library addresses the choice in Mathlib.Data.Real.Basic:
This choice is motivated by how easy it is to prove that ℝ is a commutative ring, by simply lifting everything to ℚ.
There is some further discussion of different constructions in Mathlib.Topology.UniformSpace.CompareReals, hinting that Dedekind hasn't been done:

Thesaurius
1 年前
I personally really like the construction using Cauchy sequences, because to me it is the most clear one. But the Cauchy Reals have less constructive power than Dedekind Reals, in the sense that without assuming further axioms, the second implies the first, but not the other way round. There are a dozen or so ways to construct the Reals, and they form a hierarchy of strength, Dedekind Reals being on the top (together with a few other constructions).
The comparisons are done in a paper where there is also a strict definition of strength, but I unfortunately can't find it anymore. Also: In the classical setting of ZFC, all the constructions are equivalent, so as long as you only do classical math, it doesn't really matter which one you use.
(引用終り)
以上