5 ms·
Doing a math assignment with the Lean theorem prover
- logicchains 7y agoFor people interested in using Lean, note that there's a community fork (https://github.com/leanprover-community/lean https://github.com/leanprover-community/lean) of the last official Lean 3 release 3.4.2 (https://github.com/leanprover/lean https://github.com/leanprover/lean). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (https://github.com/leanprover/lean4 https://github.com/leanprover/lean4), and it's not clear when that will be ready).
- dhosek 7y agoIt's a pity that the author's high school didn't use geometry as the means of introducing the concept of mathematical proof. The classical high school two-column proof is in many ways quite similar to the methods of Lean, albeit with a different structure.
- aadams 7y agoWill you provide links?
- lordnacho 7y agoDoes Lean allow you to put in geometric proofs? Say someone draws some circles and some lines and wants to prove that some property of the intersection points is true, eg that are always on the same straight line?
- h91wka 7y agoQuick search reveals that some people have encoded Euclid's axioms in Coq (Lean and Coq are based on roughly the same theory): http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/
- Smaug123 7y agoI greatly recommend Lockhart's Lament (https://www.maa.org/external_archive/devlin/LockhartsLament.pdf https://www.maa.org/external_archive/devlin/LockhartsLament....) which says exactly the opposite. I didn't personally undergo "two-column proof" education, and learned what the phrase means from Lockhart's Lament itself, but it sounds miserable; I say this as an MMath who specialised in set theory and logic, and who has been side-project formalising maths in Agda for the last two years.
- JadeNB 7y ago> I didn't personally undergo "two-column proof" education, and learned what the phrase means from Lockhart's Lament itself, but it sounds miserable; I say this as an MMath who specialised in set theory and logic, and who has been side-project formalising maths in Agda for the last two years. As a professional mathematician who did go through two-column proof, you're not the only one who finds them miserable. Personally, abstract algebra was what won me over to the beauty of proof (probably that old standby, the irrationality of sqrt(2), was the first); but everyone will find a different experience.
- dhosek 7y agoAesthetically, two-column proofs are miserable, but they have the advantage that the logic is very clearly laid out. There's no chance to hand-wave when every step of the proof needs to be explicitly justified.
- 0az 7y agoI personally credit my own geometry education, as much as I disliked it, with giving me the tools I needed to succeed in Calculus. That Calculus final involved proving part two of the FTC. Fun times. AP Calculus? It's much less helpful, in its computational focus.
- outlace 7y agoI just started learning Lean today - what a coincidence. I have found learning lean difficult but gratifying. The post serves as further motivation.
- abjKT26nO8 7y agoIt's a bit ironic, but the author repeated the same error every time they wrote the formula involving sigma. What they wanted to write was $\sum_{0}^{n} k$. What they actually wrote ($\sum_{0}^{n} n$) is equal to $n \cdot (n+1)$ (without the division by 2).
- masteranza 7y agoThe example the author provided is too trivial to convince me to use lean.
- kevinbuzzard 7y ago[Here](https://arxiv.org/abs/1907.01449 https://arxiv.org/abs/1907.01449) is a Lean formalisation of a 2017 Annals of Mathematics paper.
- wwarner 7y agoThis is really futuristic. Feels like it could be applied to model based design.
- xvilka 7y agoThe same can be done also with Coq[1], it is easy to learn[2], actively developed[3], and better documented[4]. You can also visit their discussion board[5]. Regarding the usual Lean vs Coq "war" and so-called "setoid hell" you can read a lengthy discussion on their GitHub[6]. [1] http://coq.inria.fr/ http://coq.inria.fr/ [2] https://learnxinyminutes.com/docs/coq/ https://learnxinyminutes.com/docs/coq/ [3] https://github.com/coq/coq https://github.com/coq/coq [4] https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/ [5] https://coq.discourse.group/ https://coq.discourse.group/ [6] https://github.com/coq/coq/issues/10871 https://github.com/coq/coq/issues/10871
- ahelwer 7y agoI tried learning Coq through the Software Foundations track a couple times and enjoyed what I did learn, but bounced off. If Coq made something similar to the Natural Number Game [0] I'd love to give it a go and see the differences! [0] https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
- ivanbakel 7y agoThat final link is very insightful. Not to pick sides, but if Lean really doesn't have subject reduction when you use quotient types, that's a crazy property to drop (or lose accidentally).
- ocfnash 7y agoI have a little experience of both Coq and Lean and have followed some of the discussion about Lean's handling of quotient types. I have seen computer scientists emphasise to mathematicians that subject reduction should not be forfeit but I have yet to see a convincing argument/example for why not. I don't suppose you can elaborate on why this may be / is so crazy, that someone with only a limited understanding of type theory might follow?
- zozbot234 7y agoSetoids are also very relevant in constructive math, for similar reasons. Quotient types/sets basically conflate cases where one can easily normalize the elements of some equivalent class vs. cases where this cannot be done effectively, and that's not a good approach at all.