3 ms·
An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other sligh
by rao-v 29d ago
An aside on Lean and it's massive library of results: As someone who's put non trivial effort into slowly learning geometric algebra, lie theory and other slightly advanced math topics, I have to say my brain cannot read Lean. It feels so unprocessable.
I've tried the various intros to Lean multiple times (even before Lean 4 came out) and something about the way Lean proofs are written does not align with how I think about proofs. My very brief attempts at Isabelle / RCoq feel more natural.
I think it's a pity that the future of proofs is Lean. I'd love for someone to come up with a more digestable proof language!
- gowld 29d agoThat's like saying the future of code is Assembler. Lean is not for humans.
- epgui 29d agoLean is for humans.
- SirHackalot 29d agoInteresting to find this comment, I’ve been dipping my toes into formal methods and was doing a RCoq tutorial yesterday (really basic stuff), and I also noticed that the proofs in RCoq have a more pen -and-paper proof feel to them.
- rao-v 29d agoRight? Might be worth another shot
- c7b 29d agoIf you're doing it for fun anyway, why not use the language that gives you the most pleasure?
- voxl 29d agoHearing someone say "the future of proofs is Lean" is a bit like hearing someone say "the future of programming is Rust." Sorry to disappoint, or happy to inform, there are hundreds of programming languages actively being used, and Rust is not even the most used language. To think that proof assistants, fancy programming languages, would be any different is suspiciously motivated.
- rao-v 27d agoI hear you but point me to one novel formalization right now that is not Lean. It’s really becoming a refacto standard. Which is lovely but terrible for pedegogy
- voxl 27d ago??? Look at any conference that publishes mechanized results? You'll see plenty of Isabelle, ACL2, Rocq, Agda. You exist in the pop science bubble. If Lean has done anything it's advertised itself well. It did a good job of that as far back as the Liquid Tensor Experiment, and it's pissed many people off in the community with it's marketing antics.
- HotHotLava 29d agoThe nice thing is, once all of these proofs are formalized in a machine-checkable language, it should be relatively straightforward to translate the corpus between different languages, if someone finds something with a nicer syntax.
- auggierose 29d agoI hear you. :-)
- robinzfc 29d agoThere are a couple of proof languages that are designed for formalized mathematics (rather than formal verification of software) and to be readable by mathematicians. For example, look at the proof that square root of 2 is not rational written in Naproche (retyped from [1], typos are mine): Theorem. $\sqrt{2}$ is irrational. Proof. Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction. Qed. Or, say Isar in Isabelle/ZF [2]. There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are. [1] https://ceur-ws.org/Vol-448/paper10.pdf https://ceur-ws.org/Vol-448/paper10.pdf [2] https://isarmathlib.org/UniformSpace_ZF_1.html https://isarmathlib.org/UniformSpace_ZF_1.html [3] https://mathoverflow.net/questions/513742/are-we-stuck-with-lean https://mathoverflow.net/questions/513742/are-we-stuck-with-...