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

21–30 of 73 posts

Re: Are We Stuck with Lean?

#21

Post by andrewla »

HappyPanacea wrote: post #18
IsTom wrote: post #5

So that link( https://infosec.exchange/@0xabad1dea/117002106099986943 ) buried in the comments of comments sounds pretty damning.

https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions

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.

Metamath (and specifically Metamath Zero) is formally verified.

Re: Are We Stuck with Lean?

#22

Post by solomonb »

eru wrote: post #14
ux266478 wrote: post #3

> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed…

I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.

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.uk/slindley/papers/hasochism.pdf

Re: Are We Stuck with Lean?

#23

Post by HappyPanacea »

andrewla wrote: post #21
HappyPanacea wrote: post #18

Earlier quoted context omitted.

https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions

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?

Re: Are We Stuck with Lean?

#24

Post by applfanboysbgon »

data-ottawa wrote: post #17
eru wrote: post #13

Earlier quoted context omitted.

> Cars and non drivers in cities are the typical example. Have a look at Dutch cities for how to avoid this.

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/

Re: Are We Stuck with Lean?

#25

Post by quasisphere »

voxl wrote: post #19
quasisphere wrote: post #12

Earlier quoted context omitted.

Agreed. In addition I think a big reason why we are discussing formalization so much at the moment is that it has only recently become viable to do large scale formalization of mainstream mathematics, using LLMs. These same LLMs will make it much easier to translate from one language to another and port even larger codebases over. My prediction would therefore be that the LLMs will let us work more-or-less using stan…

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 research mathematician could actually use in real time along actual math research. 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, both individually and collaboratively (such as the recent Tau Ceti project).

Anyway, what do you mean by 'say it's a proof of something'? If you mean this in technical sense, there are plenty of examples around where single individuals or small teams have autoformalized theorems with tens or hundreds of thousands of lines Lean code that pass a comparator challenge (so the theorem is correct). If you mean this in the sense that the proof is also a proof in the eyes of humans, so that someone has actually read or understood the proof, I'm willing to acknowledge that in this area there is much work still to do. In my own experience the current LLMs are already very strong at formally proving theorems (with correct semantics), but they are still lacking in writing human-readable math prose based on these formalizations, for instance.

Re: Are We Stuck with Lean?

#26

Post by wk_end »

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.

I don't know about forcing, but there's certainly a long history of emacs users trying to convince vim users that they're wrong. Without loss of generality - the same is true in the other direction of course.

Software devs are more than used to having a multitude of tools at our disposal (text editors, programming languages, Linux distros...), having strong preferences, and engaging in the delicate balancing act of advocating for our favourites while living-and-letting-live as the cosmic ballet goes on. It's part of our culture; I don't think that culture necessarily exists outside. For instance, a common layman question to ask is, "Why are there so many programming languages? Why doesn't everyone just use the same one?" And I don't think mathematicians are immune to this blind spot.

The nearest equivalent to "tooling" in math, traditionally, would be notation I suppose, and mathematicians are accustomed to eventually coalescing around a single standard notation.

Re: Are We Stuck with Lean?

#27

Post by andrewflnr »

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…

Presumably because of potential network effects that would result from everyone being able to work in a single system. I don't think it's strange or implausible for people to want that.

Re: Are We Stuck with Lean?

#28

Post by pverheggen »

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?

Re: Are We Stuck with Lean?

#29

Post by ux266478 »

eru wrote: post #14
ux266478 wrote: post #3

> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean Isn't the entire point mathematicians adopted Lean where they spurned Haskell is because of the batteries-included ZFC object language in the former? Metamath implements a set theory object language just the same, it's not based on it at all in this sense. You just changed…

I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.

That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviously, but that's not an expressibility problem, and I wouldn't really equate what remains practical with triviality. With language extensions, you can just kind of do whatever as shown by Liquid Haskell.

I can see the real pain point more being the fact that it's not like a typical proof assistant, and utilizing it as one is going to be unintuitive and strange.

https://hackage.haskell.org/package/type-settheory

Re: Are We Stuck with Lean?

#30

Post by ux266478 »

solomonb wrote: post #22
eru wrote: post #14

Earlier quoted context omitted.

I don't think Haskell would have been useful anyway? You'd want a dependently typed language for this, not Haskell. Haskell's types can't really express anything non-trivial.

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.
Post reply on HN