4 ms·
Highly recommend Lean theorem prover for programmers who want to self-learn some mathematics
by outlace 5y ago
Highly recommend Lean theorem prover for programmers who want to self-learn some mathematics
- fogof 5y agoI want to second this. I started working on a project in Lean only last December. Since then, I've made several contributions to the mathlib github repo - the first time I've contributed to open source despite wanting to get into it for a few years. The Zulip forum https://leanprover.zulipchat.com/# https://leanprover.zulipchat.com/# is very welcoming and responsive to questions. If you're interested in mathematics and you want to contribute to the growing hivemind working on this kind of thing, I highly encourage you to learn Lean and join this community.
- zozbot234 5y agoI'm not sure if I would recommend that, given that Lean has less support for constructive math than some existing systems, and constructive math can be very convenient for proving stuff about programs/computations.
- penisverse 5y agoAt least it's easy to use, i can't for the life of me install and set up agda for example.
- creata 5y agoThis is way off topic, but that's funny, because it's the other way around for me: I can install Agda with a `pacman -S agda`, but I'd need to go through the AUR for Lean.
- IngoBlechschmid 5y agoFor this reason, I decided to make Agda playable in the browser here: https://agdapad.quasicoherent.io/ https://agdapad.quasicoherent.io/ Enjoy! :-)
- outlace 5y agoThats not true… in Lean you can restrict yourself to constructive math if you want to for some reason. Just that most actual mathematicians don’t.
- creata 5y ago> constructive math can be very convenient for proving stuff about programs/computations. How? I can see how proving properties of programs is a place where constructivism won't get in the way, but do you have an example of where it can be more convenient?
- logicchains 5y agoThe Howard-Curry correspondence only applies if you stick to constructive maths. This means all your proofs are also programs (and computable) for free. E.g. if trying to prove "blah(x) = blaz(x)" for a fixed x, where blah and blaz are both computable predicates, then the proof can be solved easily just by evaluating blah(x) and blaz(x). This can't be done if blah or blaz isn't computable.
- creata 5y agoSure, but isn't it the case that either your predicates are computable, in which case both a "classical" and a "constructive" proof assistant could evaluate them, or they're not, in which case neither could evaluate them?
- logicchains 5y agoYep, but one could express a computable predicate classically (e.g. by unnecessarily invoking the axiom of choice in its definition). Using a constructive proof assistant prevents accidentally doing this, and encourages using constructive definitions where possible. It also encourages using computable mathematical formulations (e.g. computable reals vs classical reals).
- ProfHewitt 5y agoThe Howard-Curry correspondence does not help proving properties of concurrent systems. Instead, need to use Actor Event induction: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003
- ProfHewitt 5y ago
- mbrodersen 5y agoReal mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.
- zozbot234 5y agoThe mathematicians who study topos theory, the 'internal logic' of whatever category etc. are definitely "real" mathematicians, and they have to care about constructive settings because these come up very naturally in that field. Constructivism is not an isolated niche anymore, it interacts with "real" math too.
- mbrodersen 5y agoAgree! I am learning a lot just reading through the mathlib definitions and playing around with proving simple compilers correct.