3 ms·
> With code, I do this on a regular basis. With mathematics, it is plain impossible. It's easily possible with systems like Coq [1] plus a nice IDE [2]. There
by xvilka 6y ago
> With code, I do this on a regular basis. With mathematics, it is plain impossible.
It's easily possible with systems like Coq [1] plus a nice IDE [2]. There are mathematical libraries for the foundations [3][4].
[1] https://github.com/coq-community/awesome-coq https://github.com/coq-community/awesome-coq
[2] https://github.com/coq-community/vscoq https://github.com/coq-community/vscoq
[3] https://github.com/UniMath https://github.com/UniMath
[4] https://github.com/math-comp https://github.com/math-comp
- pwdisswordfish2 6y agoThat only works if someone bothered to write their proof in Coq in the first place. Most don’t.