Hacker GitHub

← All repos

leanprover/lean3

View on GitHub ↗ ★ 2,152 C++ archived

Lean Theorem Prover

15 mentions on Hacker News by 12 people: 2 stories, 13 comments · first 2014-06-21 · latest 2020-11-21

Mentions per year 15 mentions · busiest year 2020 (5)
20082026
AllStoriesComments NewestTopOldest
  1. …actually a theorem. It follows from functional extentionality and the existence of quotient types. https://github.com/leanprover/lean/blob/master/library/init/... The axiom of choice is an actual axiom, and it too ends up being used…
    comment by kmill · 2020-11-21 · in Why is dependent type theory more suitable than set theory for proof assistants?
  2. Plus, it's a theorem in Lean: https://github.com/leanprover/lean/blob/master/library/init/... (Lean has a somewhat different type theory from Coq, where propositions in Prop have the property that all proofs of a property are defined to be…
    comment by kmill · 2020-07-11 · in Hindley-Milner Type Inference (2012)
  3. …has a pretty strong commitment to constructability, has the law of the excluded middle just fine: https://github.com/leanprover/lean/blob/master/library/init/... The caveat is that it only exists in Prop, and it's a consequence of proof…
    comment by kmill · 2020-07-11 · in Hindley-Milner Type Inference (2012)
  4. …fork ( https://github.com/leanprover-community/lean ) of the last official Lean 3 release 3.4.2 ( https://github.com/leanprover/lean ). The fork is still under active maintenance, so might be a better place to start (the main development…
    comment by logicchains · 2020-04-06 · in Doing a math assignment with the Lean theorem prover
  5. …is probably something along the lines of: if you want performance, use a low-level language. [1] https://github.com/leanprover/lean/tree/master/src [2] https://github.com/leanprover/lean4/tree/master/src
    comment by Cladode · 2020-01-24 · in Haskell Problems for a New Decade
  6. ▲ 2
    Lean Theorem Prover
    story by tosh · 2019-10-14 · 0 comments
  7. …(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…
    comment by MayeulC · 2019-10-09 · in The Future of Mathematics? [video]
  8. …c++ in a significant way in the long run. To close of with an example the lean theorem prover https://github.com/leanprover/lean , implemented in C++ handily beats the 20+ year old Coq prover. One of its key features is multicore support.…
    comment by orbifold · 2018-11-08 · in Is it time to rewrite the operating system in Rust? [slides]
  9. As far as C++ code goes, the Lean Prover is really well maintained: https://github.com/leanprover/lean I'd also say GHC is quite good. And Pandoc as well. I don't think I can compute enough variables to consider the "highest" though... so…
    comment by agentultra · 2018-09-21 · in Ask HN: What open source project, in your opinion, has the highest code quality?
  10. …Lean 4, is currently under development, which will presumably replace Lean 3 once complete: https://github.com/leanprover/lean/blob/master/doc/lean4.md .
    comment by logicchains · 2018-05-29 · in Theorem Proving in Lean
  11. No, it's not true, it "extracts" (compiles) to C++. < https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the Lean library ("runtime") for some objects, otherwise…
    comment by cmrx64 · 2017-07-21 · in Coq-based synthesis of Scala programs which are correct-by-construction [pdf]
  12. …you to compile all the constructions you can formalize in Lean directly to native code. (see https://github.com/leanprover/lean/pull/1241 for progress) (Note that none of those code extractors are verified to be correct themselves, lacking…
    comment by tehmillhouse · 2017-07-21 · in Coq-based synthesis of Scala programs which are correct-by-construction [pdf]
  13. …not sufficient to overcome the steep learning curve of these tools. I have some hopes in [lean]( https://github.com/leanprover/lean ), a new proof assistant inspired from Coq, which puts the focus on good UI and automation.
    comment by c-cube · 2017-05-15 · in Why do many math books have so much detail and so little enlightenment? (2010)
  14. There is a PR for a Lean backend producing both C++ and Rust: https://github.com/leanprover/lean/pull/1090 Note, however, that this is purely focused on executing Lean code, not integrating with other C++/Rust sources.
    comment by derkha · 2016-07-22 · in A Formal Verification of Rust's Binary Search Implementation
  15. ▲ 1
    Lean Theorem Prover
    story by luu · 2014-06-21 · 0 comments