Self-contained "minimal" implementation of ℝ in Lean?

Stream: new members

[Isak Colboubrani]

Are there any book chapters, lectures, code examples, or other resources that cover the construction of the real numbers from scratch using Cauchy sequences with rational numbers in Lean (preferably Lean 4, though Lean 3 is acceptable)? Ideally, I am seeking a resource that relies solely on the Lean 4 core, without any other dependencies.

I am aware of the construction in Mathlib, but it is very general (for valid reasons) and likely not minimal in terms of lines of code. I am looking for a minimal and self-contained implementation that follows the "shortest formalized route" to the real numbers while being instructive for undergraduate students.

[Isak Colboubrani]

I would like to add that a heavily sorry-filled, self-contained implementation of the real numbers would also suffice if available. I have searched, but all I can find is the Mathlib implementation.

[Isak Colboubrani]

I have compiled a list of all known implementations of the real numbers in Lean.

Does this list appear to be complete for publicly available implementations of the real numbers in Lean?

I had expected, or perhaps hoped, to find a "from scratch" implementation as part of the Xena project (Imperial), but after searching the Xena project blog, I couldn't find any evidence of such an implementation. It is possible that the real numbers were already included in Mathlib when the Xena project/Imperial undergraduate formalization effort began.

Current implementation in mathlib (Lean 4, credits: Mario Carneiro, Floris van Doorn):

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Real/Basic.lean

Lean 3 implementation from 2017 ("construct reals as complete, linear ordered field", credit: Johannes Hölzl):

https://github.com/leanprover-community/mathlib/commit/7882677de6cdb4f0044726054e16a535407256c0

Lean 3 implementation from 2018 ("feat(data/real): reals from first principles", credit: Mario Carneiro):

https://github.com/leanprover-community/mathlib/commit/04cac9587e1d32479935a0cf132b140b28bbac2b

Does this look correct?

[Yaël Dillies]

Nope, you're missing the Eudoxus reals, implemented twice (search through Zulip)

[Kevin Buzzard]

Oh yes Imperial students did Eudoxus twice, and there may be more implementations. Yes Isak you're right, when I got interested in lean Johannes Hoelzl had just finished making the real numbers in mathlib. My first PR to mathlib was the complex numbers :-)

[Isak Colboubrani]

Thanks for the clarification @Yaël Dillies and @Kevin Buzzard!

I located the Eudoxus reals implementation by Xiang Li on GitHub. However, based on the Zulip archive, it appears that the other Eudoxus implementation by an Imperial student was never publicly released.

From my investigation, it seems there is only one publicly accessible Lean 4 implementation of the real numbers, which is the one in mathlib attributed to Mario Carneiro and Floris van Doorn. Is this statement accurate?

Links of relevance:

Eudoxus reals (Lean 3, credit: Xiang Li)
https://github.com/Lix0120/eudoxus

Axiomatization of the real numbers: linear ordered field (credit: Alex J Best)
https://github.com/leanprover-community/mathlib/pull/3292

[Kevin Buzzard]

I don't know of any other Lean 4 developments of the real numbers, although @Isak Colboubrani has got it on their radar I believe...

[Patrick Massot]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/building.20reals.20with.20quasi-morphisms for yet another implementation of Eudoxus reals.

[Isak Colboubrani]

Thanks @Patrick Massot! Are you referring to the code in this message, or is there additional code outside of that thread that I should be aware of?

I attempted to port it to Lean 4. Does it look like a correct translation? Please let me know if anything appears odd or non-idiomatic: I'm eager to learn!

-- Lean 4 port of https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/building.20reals.20with.20quasi-morphisms/near/256852903

import Mathlib

structure QuasiMorphism where
  toFun : ℤ → ℤ
  bound : ℤ
  mapMul' : ∀ x y, abs (toFun (x * y) - toFun x - toFun y) ≤ bound

instance : CoeFun QuasiMorphism (fun _ => ℤ → ℤ) where
  coe := fun q => q.toFun

lemma mapMul (q : QuasiMorphism) (x y : ℤ) : abs (q (x * y) - q x - q y) ≤ q.bound := q.mapMul' x y

instance QuasiMorphismSetoid : Setoid QuasiMorphism where
  r := sorry
  iseqv := ⟨sorry, sorry, sorry⟩

def EuxodusReal := Quotient QuasiMorphismSetoid

variable (q : QuasiMorphism)

#check (⟦q⟧ : EuxodusReal)

[Patrick Massot]

I don't know, you need to ask Yannis.

[Jihoon Hyun]

You might want to take a look at this, although it is explained in Coq.

[Dean Young]

Is there one using binary expansions and the order topology?