Viewing profile — leanuser57

Here is a "nonsense" theorem that is provable in Lean: “There exists a real number r such that 1/r = 0.” If you try to translate this theorem into maths, you will run into trouble …

In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compos…

First of all, I wish you luck and strength. I can't really imagine how this must be for you. One little pointer: I know that edbrowse is developed by a blind programmer. It might t…

No, they mean elliptic curves defined over number fields that don't embed into the reals.

Note that https://leanprover.github.io is all about the frozen version of Lean 3, while the devs are working on Lean 4. In the mean time, the community is maintaining a fork of Lea…

Note that the levels are "fake", so if you lost your progress that's sad, but you can just skip ahead to where you left. (We're looking into adding localStorage or something like t…