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
20082026
-
…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? -
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) -
…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) -
…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 -
…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 -
…(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] -
…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] -
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? -
…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 -
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] -
…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] -
…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) -
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