LEAN3

Stream: general

[Mohamamd Awheeo]

How to represent different numbers in LEAN3 I know that I can use \nat for natrual numbers but what about irrational numbers, real numbers and prime and others?

[Yaël Dillies]

Irrational number will be {x : ℝ | irrational x}. See docs3#irrational

[Mohamamd Awheeo]

but it does not work:
image.png

[Eric Wieser]

You will need import data.real.irrational

[Eric Wieser]

@Kevin Buzzard, is the Lean 4 version of https://github.com/ImperialCollegeLondon/M40001_lean available, or did your FLT funding result in it being canned?

[Kim Morrison]

@Mohamamd Awheeo, unless there is some particular reason you need to be using Lean 3, it might be helpful to learn that Lean 3 is obsolete, and everyone is using Lean 4 now.

[Kevin Buzzard]

IIRC I didn't make a lean 4 version of that repo

[Eric Wieser]

Perhaps it's worth removing the promise in the readme that you were going to

[Eric Wieser]

(relatedly, https://github.com/ImperialCollegeLondon/formalising-mathematics-2023/pull/2 adds a link to the lean4 version of your other course)

[Yury G. Kudryashov]

BTW, the theorem you formulated is incorrect: $\sqrt{2}$ and $1/\sqrt{2}$ are irrational and their product is $1$.