Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

kirancodes.me

Post reply on HN
Print view View original

11–18 of 18 posts

Re: How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

#11

Post by yuppiemephisto »

gopiandcode wrote: post #7
gnulinux wrote: post #2

I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decades. I really wish more programmers and mathematicians knew about automated theorem proving and automated reasoning. It's nothing short of revolutionary and I think next generation of pure mathematicians will use these as a crucial tool in their research. [1] I…

Oh, really? I'm curious what exactly you mean by limitless metaprogramming. I've really been drawn into Lean specifically because of how easy to extend and malleable the language itself is, so if Agda is even more so then I'd be really eager to try that out. e.g.: - embedding a prolog/asp DSL: https://github.com/kiranandcode/cleango - embedding a tex/latex DSL: https://github.com/kiranandcode/LeanTeX

I was surprised to hear their claim about Agda's metaprogramming, I say lean is better here

Re: How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

#12

Post by sega_sai »

gfaster wrote: post #6
sega_sai wrote: post #4

Interesting. I always wanted to try Lean, and personally never found an easy way to do it, as it requires installing a plugin in vscode, create a project or reading the lean book. But following the links I've found this nice interactive tutorial for proving 2+2=4 in Peano arithmetic: https://adam.math.hhu.de/#/g/leanprover-community/nng4/ It's quite instructive.

Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin. If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on. [0]: https:…

I've seen the book, but I've personally found it not very useful for a person who wants to first get the basics.

The natural number's game is actually quite fun, and I did understand much better the language. And it's also interactive, so you can try your solutions, and there are hints when stuck.

Re: How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

#13

Post by m_j_g »

gnulinux wrote: post #2

I personally prefer Agda to Lean or Coq [1] to prove my theorems but this frontier is imho among the most exciting research in theoretical CS in many many decades. I really wish more programmers and mathematicians knew about automated theorem proving and automated reasoning. It's nothing short of revolutionary and I think next generation of pure mathematicians will use these as a crucial tool in their research. [1] I…

Did you played with cubical flavor of Agda? here is fun project of mine related to it : https://github.com/marcinjangrzybowski/cubeViz2 :)

Re: How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

#14

Post by Tainnor »

I have a pet (undergraduate complex analysis) formalisation project in Lean, purely for didactic and recreational purposes. I find it rewarding in the same way others may find it rewarding to train for a triathlon - it's often extremely grueling work and it can take forever to make even modest progress. When I actually do get to a "big" result such as defining pi (from scratch) or Cauchy's integral theorem it feels rewarding, but there's a ton of torn out hairs along the way, when linarith is stupider than it should be, I need to spend forever to prove very obvious things, I can't find the tactic I need in mathlib or I realise there's barely anything about triangles in there. For somebody like me without a PhD it also doesn't help that mathlib almost always goes for full generality which makes it hard to use it effectively (although I do understand the reason for it).

I think this is all very exciting but I also think ergonomics will probably need to improve quite a bit before Lean will become mainstream in mathematics.

Re: How to (actually) prove it – New Frontiers of Mathematics and Computing in Lean

#18

Post by Tainnor »

moi2388 wrote: post #17
Tainnor wrote: post #16

Earlier quoted context omitted.

did you read the wrong article?

[flagged]

No idea why you're picking on the author's minor grammar mistakes. They may not even be a native speaker. The article is perfectly understandable, I read it myself and didn't even notice the errors before you pointed them out.

> “ Of course, mathematicians gain a lot by doing this1, machine checked proofs reduce..”

This sentence is grammatical, the 1 is just a footnote (which you can click) - this could be improved typographically, I suppose. The rest are just minor mistakes - "are promising to", "with the Lean Theorem prover", "to non-mathematicians".

Post reply on HN