coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Lean Theorem Prover

From: Saulo Araujo <saulo2 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Lean Theorem Prover
Date: Wed, 24 Feb 2016 21:17:07 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=saulo2 AT gmail.com; spf=Pass smtp.mailfrom=saulo2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f49.google.com
Ironport-phdr: 9a23:n5lioRBG5Ksqxzyqq8ZOUyQJP3N1i/DPJgcQr6AfoPdwSP74pcbcNUDSrc9gkEXOFd2CrakU1KyL4uu5CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb3jsMSCKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs0AVT2ER2jNSChXH61muRZ7stiygnuV40Siee8bxSOZnCnyZ8653RUqw2288PDkj/TSPhw==

Hi,

I recently discovered the Lean Theorem Prover (https://leanprover.github.io/about/). I did some toy experiments with it and and, at least in this first contact, it seemed similar to Coq. I am curious about how the Coq community sees Lean. Does it see Lean as "competitor" of Coq? Is it possible for Coq to bridge the gap betweem interactive and automated theorem proving like Lean aims to do?

Saulo

[Coq-Club] Lean Theorem Prover, Saulo Araujo, 02/25/2016
- Re: [Coq-Club] Lean Theorem Prover, Jonathan Leivent, 02/25/2016
  - RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Benjamin Pierce, 02/25/2016
      - RE: [Coq-Club] Lean Theorem Prover, Soegtrop, Michael, 02/25/2016
  - Re: [Coq-Club] Lean Theorem Prover, Freek Wiedijk, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Théo Zimmermann, 02/25/2016
    - Re: [Coq-Club] Lean Theorem Prover, Bas Spitters, 02/25/2016
      - Re: [Coq-Club] Lean Theorem Prover, roux cody, 02/25/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016
        
        Re: [Coq-Club] Lean Theorem Prover, Clément Pit--Claudel, 02/25/2016