leanuser57

8 ms·

1. 1.▲
   by leanuser57 6y ago

   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
2. 2.▲
   by leanuser57 6y ago

   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.
3. 3.▲
   by leanuser57 6y ago

   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://
4. 4.▲
   by leanuser57 6y ago

   No, they mean elliptic curves defined over number fields that don't embed into the reals.
5. 5.▲
   by leanuser57 6y ago

   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 o
6. 6.▲
   by leanuser57 6y ago

   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.