[HN Gopher] Lean - Theorem Prover
___________________________________________________________________
Lean - Theorem Prover
Author : thunderbong
Score : 51 points
Date : 2023-01-20 17:34 UTC (5 hours ago)
(HTM) web link (leanprover.github.io)
(TXT) w3m dump (leanprover.github.io)
| nolroz wrote:
| Sheesh. I got all excited thinking that Lean was working on
| "Thorium Power".
| nequo wrote:
| The _Type Theory Forall_ podcast published an interview this week
| with Kevin Buzzard who has been coordinating the mathlib
| efforts[1] for Lean. If you 're interested in math, theorem
| provers, or Lean, then it is worth listening to:
|
| https://www.typetheoryforall.com/2023/01/16/26-Kevin-Buzzard...
|
| [1] https://leanprover-community.github.io/
| agentultra wrote:
| Also interesting as a programming language:
|
| Lean 3: https://agentultra.github.io/lean-for-hackers/
|
| Lean 4: https://agentultra.github.io/lean-4-hackers/
| daxfohl wrote:
| Is the experience here much different from Idris? The latter
| was more a language that can also be used for proofs, whereas
| Lean came out of a proof assistant. Does that lead to much
| difference in use, or do the approaches essentially converge?
|
| Looking briefly at the example code, it seems pretty similar.
| agentultra wrote:
| I think they end up similar. Although Lean 3 is much more
| geared towards writing proofs with the addition of mathlib
| [0] which aims to be a library of formalized mathematics.
|
| [0] https://github.com/leanprover-community/mathlib
| schoen wrote:
| If you want to try it out and have never used a theorem prover,
| consider trying the Natural Number Game.
|
| https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...
| dang wrote:
| Related:
|
| _The future of interactive theorem proving?_ -
| https://news.ycombinator.com/item?id=32489099 - Aug 2022 (16
| comments)
|
| _The Lean Theorem Prover_ -
| https://news.ycombinator.com/item?id=30752610 - March 2022 (1
| comment)
|
| _Propositional logic exercises with the lean theorem prover_ -
| https://news.ycombinator.com/item?id=28951457 - Oct 2021 (8
| comments)
|
| _The Natural Number Game_ -
| https://news.ycombinator.com/item?id=27504877 - June 2021 (2
| comments)
|
| _A Review of the Lean Theorem Prover_ -
| https://news.ycombinator.com/item?id=25550240 - Dec 2020 (11
| comments)
|
| _Lean is better for proper maths than all the other theorem
| provers_ - https://news.ycombinator.com/item?id=22802490 - April
| 2020 (1 comment)
|
| _Natural number game_ -
| https://news.ycombinator.com/item?id=22801607 - April 2020 (14
| comments)
|
| _Lean Book: The Hitchhiker 's Guide to Logical Verification
| [pdf]_ - https://news.ycombinator.com/item?id=22794533 - April
| 2020 (19 comments)
|
| _Doing a math assignment with the Lean theorem prover_ -
| https://news.ycombinator.com/item?id=22789953 - April 2020 (29
| comments)
|
| _Coq is a Lean Typechecker_ -
| https://news.ycombinator.com/item?id=22171305 - Jan 2020 (31
| comments)
|
| _Theorem Proving in Lean [pdf]_ -
| https://news.ycombinator.com/item?id=21108357 - Sept 2019 (22
| comments)
|
| _Theorem Proving in Lean_ -
| https://news.ycombinator.com/item?id=17171101 - May 2018 (30
| comments)
|
| _Theorem Proving in Lean_ -
| https://news.ycombinator.com/item?id=9424507 - April 2015 (1
| comment)
|
| _Tutorial: Theorem Proving in Lean_ -
| https://news.ycombinator.com/item?id=9288135 - March 2015 (2
| comments)
|
| Also related and interesting:
|
| https://news.ycombinator.com/threads?id=kevinbuzzard
|
| _Mathematicians welcome computer-assisted proof in 'grand
| unification' theory_ -
| https://news.ycombinator.com/item?id=27559917 - June 2021 (136
| comments)
|
| _Formalising Mathematics: An Introduction_ -
| https://news.ycombinator.com/item?id=26214593 - Feb 2021 (116
| comments)
|
| _A mathematical formalisation challenge by Peter Scholze_ -
| https://news.ycombinator.com/item?id=25322551 - Dec 2020 (24
| comments)
|
| _At the International Mathematical Olympiad, computers prepare
| to go for the gold_ -
| https://news.ycombinator.com/item?id=24544607 - Sept 2020 (64
| comments)
|
| _Division by zero in type theory: a FAQ_ -
| https://news.ycombinator.com/item?id=23745532 - July 2020 (82
| comments)
|
| _Where is the fashionable mathematics?_ -
| https://news.ycombinator.com/item?id=22390486 - Feb 2020 (64
| comments)
| zone411 wrote:
| Here is a chart of Mathlib's growth: https://leanprover-
| community.github.io/mathlib_stats.html, and here is information
| about what parts of undegrad math are covered so far:
| https://leanprover-community.github.io/undergrad.html.
___________________________________________________________________
(page generated 2023-01-20 23:00 UTC)