Hacker News new | past | comments | ask | show | jobs | submit login

A few links (the chat is mentionned multiple times during the chat)

Lean: https://leanprover.github.io/

Repo: https://github.com/leanprover/lean/

Chat: https://leanprover.zulipchat.com/

The maths course (in French) that can be seen during the presentation: https://www.math.u-psud.fr/~pmassot/enseignement/math114/

License: Apache 2.0

I was afraid there would be a CLA, as is customary with Microsoft's projects (and the main reason I didn't contribute to any), but I couldn't find one. Good call.

> Lean 4

> We are currently developing Lean 4 in a new (private) repository. The source code will be moved here when Lean 4 is ready. Users should not expect Lean 4 will be backward compatible with Lean 3. [Committed one year ago]

Really, really not a fan of this. This basically prevents anyone from attempting to add new features or fixes, as they might be obsolete by the time the new version comes out (incompatible or already fixed).

Lean 4 WIP is public now: https://github.com/leanprover/lean4. But PRs aren't welcome. Personally I think Coq's done waaay better at community management.

Can I ask how Mizar compares to Lean, Coq, and Isabelle?

I've wondering about that quite a while because I knew someone who was involved in the Mizar project, but never had the time to get into automated theorem proving myself. I was impressed by the semi-natural language proofs.

Comparing these different approaches is not trivial, of course.

One view is to look at "Formalizing 100 Theorems" by Freek Wiedijk, which lists 100 mathematical theorems and the various systems that have formalized a nontrivial number of them. It's basically a "challenge list" for these kinds of systems:


This list is discussed in "Formal Proof - Getting Started" (Freek Wiedijk, Notices of the AMS, Volume 55, Number 11, December 2008).

That list is absolutely not the only way to compare different tools. Still, it gives you a sense of how far along each one has come in actually making proofs. Here's the current status:

    HOL Light  86
    Isabelle  83
    Metamath  71
    Coq  69
    Mizar  69
    ProofPower  43
    Lean  29
    nqthm/ACL2  18
    PVS  16
    NuPRL/MetaPRL  8
As you can see, the top ones today are HOL Light, Isabelle, Metamath, Coq, and Mizar. Lean has far fewer, but to be fair it's also much newer.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact