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

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

kirancodes.me

81 pointsgopiandcode17 comments

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] It's a personal preference but Agda is simply a much better language with almost limitless metaprogramming which allows me to write proofs close to as they'd appear in prose math papers. It has a smaller ecosystem though. I've never seen a proof in any other language I personally didn't think would be much more readable/simpler in Agda.

I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some:

https://lets-play-agda.quasicoherent.io/

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

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

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.

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://hrmacbeth.github.io/math2001/index.html

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.

Fwiw there's also an Emacs plugin which is what I use and it works really well.

For using Lean as a theorem prover, this book is pretty good: https://github.com/lean-forward/logical_verification_2024

Also, Lean is also remarkably usable as a programming language itself, which might give an easier onboarding ramp: https://lean-lang.org/functional_programming_in_lean/

Ironically, the website broke, and became stuck on the "rw[one_is_succ_zero]" rewrite rule, continually telling me that "rfl" isn't valid. Sigh.

A thing that still stands out to me is that even in this work we're looking at Lean as a way of verifying a proof, but I do not know how much exploratory work is possible in Lean.

In Rocq/Coq, I've found myself often lost in the weeds when exploring a problem just through tactics mode (half expecting it to handle the more boring machinery), and really do have to think pretty hard about how I get from A to B.

Some of this is, quite simply, me just walking in the wrong direction (if you have multiple things you can induct on, the choice can greatly affect how easy it is to move forward!). I just wish that the computer would be a bit better at helping me realize I'm in the wrong direction.

Stuff like Quickchick[0] helps, but just generally I would love the computer to more actively give me counterexamples to some extent.

[0]: https://github.com/QuickChick/QuickChick

Ahh, that is a valid point; so it's not quite as clear as using something like quick check, but it does feel like there is increasing interest and activity in people trying out doing exploratory maths in Lean itself.

I mention it in the blog post, but one project in that direction is Terence Tao's equational_theories project (https://teorth.github.io/equational_theories/), where it seems like a bunch of hobbyists and mathematicians are working together using Lean to prove new mathematics enabled by Lean.

[flagged]

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".

Reply on news.ycombinator.com