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

Are We Stuck with Lean?

mathoverflow.net

Post reply on HN
Print view View original

31–40 of 73 posts

Re: Are We Stuck with Lean?

#31

Post by wk_end »

7373737373 wrote: post #2

Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m... Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood

According to [0], "Rocq’s kernel spans approximately 41K lines of OCaml code, while Lean’s kernel consists of approximately 8K lines of C++ code."

[0] https://dl.acm.org/doi/pdf/10.1145/3747511

Re: Are We Stuck with Lean?

#32

Post by joe_the_user »

pverheggen wrote: post #28
seanhunter wrote: post #7

I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs. It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on…

I have zero experience with formal verification, just speculating here - but could it be because of the network effects? More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?

I too know nothing about formal verification but I know that mathematical proof is different individual tooling. Informal statements, Lean and whatever other formal provers are all language and languages are social so what someone uses will impact you and so it's legitimate to have an opinion.

Re: Are We Stuck with Lean?

#33

Post by data-ottawa »

applfanboysbgon wrote: post #24
data-ottawa wrote: post #17

Earlier quoted context omitted.

I immediately thought that’s not totally fair due to the size of the Netherlands vs other countries. I asked Mistral to do an analysis: nearly zero R^2 for car ownership vs log country area, and it’s the same with proportion of urban population in OECD countries. Netherlands isn’t very different from peers in car ownership, they just treat cyclists very well it seems. This is a total tangent, just found it interestin…

As it turns out, people live in cities[1]. The amount of empty space a country has outside of cities doesn't have much bearing on navigation and infrastructure inside cities. [1] https://xkcd.com/1138/

Right, but there’s zero correlation between urban population percentage and cars per capita either, which was surprising to me. I’d have expected a vague logistic curve.

Re: Are We Stuck with Lean?

#34

Post by Diogenesian »

HappyPanacea wrote: post #23
andrewla wrote: post #21

Earlier quoted context omitted.

My takeaway was not the involvement of the LLMs, which I consider to be irrelevant; the core was that there was an exploit of a flaw in the verification engine that allowed an incorrect proof to be validated. That is not great. In addition to their use as tools for pure math, they are also used for software verification, where adversarial examples could have real-world applications in verifiable supply chain attacks.…

Right, but the point is as far as I'm aware nobody accidentally found a bug in Lean by proving a theorem in a non adversarial context (and this submission is a link to a discussion at Mathoverflow). Also I think most formal verification is done using Coq and Isabelle/HOL, no?

But I think this has to be judged against an adversarial influx of LLM-assisted pseudomathematics slop vendors. A sorry-free proof in Lean (or Rocq!) whose top-level types check out is not good enough. You gotta check for compiler chicanery in all the private methods.

Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.

Re: Are We Stuck with Lean?

#35

Post by seanhunter »

pverheggen wrote: post #28
seanhunter wrote: post #7

I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs. It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on…

I have zero experience with formal verification, just speculating here - but could it be because of the network effects? More users on your preferred tool means a more comprehensive database of existing proofs, and that makes writing new proofs easier, right?

Absolutely that's the reason. But the point is the big communities (I'm thinking https://leanprover-community.github.io/ , Kevin Buzzard and all the stuff he's got going at imperial college in the uk etc, the analogous efforts around roq, agda etc which I'm not as familiar with) have made their respective choices and are just getting on with formalising maths. Then there is a vocal minority who want to sit on the sidelines and say they want all these people to use something different from what they have already decided to use. Seems weird.[1]

But yeah it is definitely easier if you just need to formalise the piece you are working on and not invent the whole universe just to bake an apple pie.

[1] And I know it's exactly the same as the people on here and other forums who say other people should down tools on project X and rewrite it in go/rust/zig/whatever. I find that weird also. Like if you want to rewrite a thing in a different language go do that by all means. But saying someone else who develops something in their own time should instead develop a different thing or use a different language is just weird.

Re: Are We Stuck with Lean?

#36

Post by solomonb »

ux266478 wrote: post #30
solomonb wrote: post #22

Earlier quoted context omitted.

Correct. There are awful tricks to write [1] dependent Haskell but even then it isn't powerful enough and has a significantly worse user experience then a proper dependently typed proof checker (as bad as the UX is on those!). That said there are other languages such as Agda, Idris, and Rocq that would be fantastic replacements to Lean, especially if you care about staying constructive. 1. https://homepages.inf.ed.ac…

I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.

Idris has pi and sigma types, dependent pattern matching, view patterns, totality checking, proof search, interactive case splitting, etc, etc.

It is orders of magnitude better then Haskell where the best you can do is hacky bullshit with singletons, GADTs, and type families.

Re: Are We Stuck with Lean?

#37

Post by wizzwizz4 »

quasisphere wrote: post #25
voxl wrote: post #19

Earlier quoted context omitted.

This is horseshit. Mathlib3 and mathlib4 all existed prior to LLMs. Unimath of Agda, mathematical components of Rocq, the list goes on. LLMs have done nothing for "making large scale mechanization viable." They have been viable. The only thing has changed is the perception of the random developer who never wanted to put the effort into learning what actually needed to be learned and are instead happy to spit our comp…

I actually noticed after I posted that I should have said 'by individuals at pace not too different from writing down a standard prose proof' or something similar to address this point. Mathlib for instance is of course a phenomenal project, but it was written by a large amount of people over many years. Granted their goal was not so much speed as it was elegance, but by 'viable' I had in mind something that a resear…

> The content in Mathlib still falls very much short of being enough for formalizing much of the actual research being done in mathematics, but people are now autoformalizing non-trivial extensions on top of that,

Formalising non-trivial extensions on top of the standard library is not hard. I could bash out an average textbook formalisation at about half reading speed. The hard part is making something elegant and general, which: and that's something that LLMs don't seem able to do.¹ (If you're lucky, the textbook you're working from has already distilled the best abstractions, and there's very little work left to do to make it good enough for a library: but such textbooks do not exist in research mathematics.)

> Granted their goal was not so much speed as it was elegance,

Do not underestimate the necessity of mathematical elegance. Mathematical notation is a tool powerful enough to teach machines to think: it is essential to make these tools elegant, or you will not be able to communicate your insight to your colleagues, and certainly not the next generation. Treating the goal of mathematics as "prove the most theorems as fast as possible" is hacking off the lower branches we should be using to climb trees, simply to harvest their fruit.

¹: Anyone familiar with my HN comment history will know that I keep banging on about "cannot in principle" and "there are deep theoretical reasons that an LLM can never". I'm not doing that here: I don't know a reason that LLMs can't produce elegant mathematical abstractions – probably because I don't understand mathematics deeply enough. "LLMs can't do this" is purely an empirical observation. (Believe me, I've read a lot of LLM-generated formal mathematics: it is invariably garbage. I just don't know why.)

Re: Are We Stuck with Lean?

#38

Post by seanhunter »

7373737373 wrote: post #20
7373737373 wrote: post #2

Metamath's Python verifier - its trusted kernel - is just 700 lines of Python short: https://github.com/david-a-wheeler/mmverify.py/blob/master/m... Metamath Zero's Haskell implementation 700, and the C implementation 1000 lines (or 1800 overall) https://github.com/digama0/mm0 How do other proof systems compare? Some bug counts: https://tristan.st/blog/in_search_of_falsehood

My favorite minimalistic example of the Metamath base language (which higher level languages can compile down to), which, saved as, say, prop.mm can be verified with the verifier: $c wff $. $( we use this $constant as a type of formula (well formed formula) $) $c ( ) ! -> $. $( brackets, negation, implication $) $v A B C $. $( $variables to be used in formulas $) wa $f wff A $. $( $floating hypothesis "wa" which says…

Fair to say that perhaps isn't selling it as much as you may think. It looks like perl that has been written by someone who is in the process of having a stroke.

Re: Are We Stuck with Lean?

#39

Post by seanhunter »

Diogenesian wrote: post #34
HappyPanacea wrote: post #23

Earlier quoted context omitted.

Right, but the point is as far as I'm aware nobody accidentally found a bug in Lean by proving a theorem in a non adversarial context (and this submission is a link to a discussion at Mathoverflow). Also I think most formal verification is done using Coq and Isabelle/HOL, no?

But I think this has to be judged against an adversarial influx of LLM-assisted pseudomathematics slop vendors. A sorry-free proof in Lean (or Rocq!) whose top-level types check out is not good enough. You gotta check for compiler chicanery in all the private methods. Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.

This is something that people have thought about a fair bit and that link does not mean what you think it means

https://lean-lang.org/doc/reference/latest/ValidatingProofs/

Lean's threat model is not that it's designed so you can just take random lean code at face value without even reviewing it or whatever. It's designed to be a proof assistant to help working mathematicians validate proofs and not validate an "honest" incorrect proof. Malicious proofs that have been specifically constructed to exploit the proof system are known to be a possibility and are considered to be bugs that people try to fix, but they are not cause for serious concern.

Re: Are We Stuck with Lean?

#40

Post by Balooga »

seanhunter wrote: post #7

I find it really strange that people who don't use lean don't just get on and use the alternatives rather that trying to get everyone who is using lean to use something else. It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs. It's important to meet reality head on: Every mathematician is not going to collaborate on the same tooling (as wonderful as that might seem on…

> It feels exactly like if all the emacs users in the world tried to force all vim users to use emacs.

That's why emacs has a vim mode[1].

[1] - https://github.com/emacs-evil/evil

Post reply on HN