4 ms·
Lean 4 seems promising, too.[1] Although it looks very much like Haskell. [1] https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.g
by nequo 4y ago
Lean 4 seems promising, too.[1] Although it looks very much like Haskell.
[1] https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/
- klyrs 4y agoYes, progress is under way! It's been a few years since I tried to plumb these depths, it's probably time to look again. But I don't need to look to know that we're not there, where "there" means both accessible and widely adopted.
- chalst 4y agoLean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project: https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.ma.imperial.ac.uk/~buzzard/xena/ He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.