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 at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.

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 compose as smoothly as homogeneous division.

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 take some time to adapt to, I guess.

https://github.com/CMB/edbrowse

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 Lean 3 with some nice features + lots of docs and other material. See https://leanprover-community.github.io/

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 that... but we aren't really coders. PRs are welcome!)