Hacker News Reader

Comment by outlace | Hacker News Reader

Highly recommend Lean theorem prover for programmers who want to self-learn some mathematics

I 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/# 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.

Agree! I am learning a lot just reading through the mathlib definitions and playing around with proving simple compilers correct.

I'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.

At least it's easy to use, i can't for the life of me install and set up agda for example.

This 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.

For this reason, I decided to make Agda playable in the browser here: https://agdapad.quasicoherent.io/ Enjoy! :-)

Thats 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.

> 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?

The 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.

Sure, 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?

Yep, 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).

The Howard-Curry correspondence does not help proving

properties of concurrent systems.

Instead, need to use Actor Event induction:

https://papers.ssrn.com/abstract=3418003

Constructivism is based on intuitionistic logic, which lacks

some important logical principles.

For example, it lacks the following principles:

     * excluded middle 
     * double negation elimination

The principles can be valuable for proving properties of

concurrent systems,

Classical logic can be embedded into Constructive logic through any one of a number of choices of double negation translations. Thus it is Constructive logic that is arguably more expressive. See https://news.ycombinator.com/item?id=26217587

Unfortunately, a theoretical embedding doesn't always accomplish the

work of Double Negation Elimination in practice.

Real mathematicians doesn’t care about constructivist. Also, Lean supports working with both. So you can choose what you want to use.

The 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.

Reply on news.ycombinator.com