Hacker News Reader

Comment by chubot | Hacker News Reader

So were the 3 withdrawn proofs the ones without Lean verification?

If so, why did they mix proofs that were verified with Lean, and proofs in natural language?

I was wondering that while reading Aaronson's blog:

Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet

It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.

View on HN

Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak. Despite the community efforts, the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved. And formalization steps are small and labor intensive, so you are often constrained in how far you can go by the volume of code you produce. It's also telling that Lean tooling isn't advanced by the labs despite the resources they put into their effort, the importance they attache to Lean and the frictions they must have run into constantly. The release feels more like a retreat by the labs.

> Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak

Can you explain this? How would having a lean proof of the program make it more likely the proof is weak?

For example mathlib doesn't develop basic theories like Riemann surfaces, and doesn't have Riemann existence theorem etc. So if you develop a complex analysis result without these there are many things you can't even talk about. Developing basic theories takes time and efforts. See Anthropic FLT proof for example. While 13 million lines headline count may contain 50% redundancies due to agent swarming, on the net they still dedicated millions lines of effort to develop basic theories. And often they developed specialized versions in concrete theories just sufficient for their needs. For example they still don't have Riemann surfaces nor Riemann existence.

13 million lines?

And people laughed at Doug Lenat and Cyc for wanting to encode all knowledge as a set of rules.

Right and these are perfect math objects: a perfect sphere has only one parameter. You can't describe a real life ball in Lean. You may be able to describe a class of real life balls using probability theory.

Having a Lean proof is an assurance that you proved something. But without going through the definitions we can't know what you proved. This part can't be mechanized. It's like a program that is compiled will likely run, but you can't say it will produce what you want. FLT stands out as everyone can read the statement. This is not true for most open math problems.

> Having a Lean proof is an assurance that you proved something. But without going through the definitions, we can't know what you proved.

Sure, even a Lean proof can be wrong. But you made it sound like that because there's a Lean proof, the claims are more likely to be wrong:

>>> Given the constraint (3.5 hours of model effort) having a Lean proof is actually a sign that some of the results are likely weak

Yes for a fixed amount of effort the more you dedicate to formalization the less room there is for exploration. So the constraint is the total budget. The other constraint is if your language doesn't have the concept of gravity it is less likely you are developing the theory of gravity. So if you want to talk about modularity lifting in Lean you need to build up theories on elliptic curves, modular forms, modular curves etc first, because the library doesn't have them even if you consider them elementary. So now if you have a Lean proof with little effort I can infer that it is unlikely to say anything deep about these subjects. If you only have a paper proof, otoh, that doesn't bound your distance from the basics for me.

Would I be correct in saying that you're making a claim about how difficult the statement is to prove, rather than the accuracy of the proof?

I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.

Yes, that is the assertion here.

> the mathlib has many gaps and lacks many basic theories. So many problems can not even be stated yet not to mention proved.

That is very useful context, thank you!

> the mathlib has many gaps and lacks many basic theories.

Filling these gaps would be a great use of llm tokens!

Tokens are not the bottleneck for filling in these gaps in mathlib. Human review and growing the specialized expertise needed for human review are. https://leanprover-community.github.io/contribute/index.html...

That seems to be a creative way to have other people review your slop.

A bit like submitting an llm written PR to an open source project without reading and understanding it.

Have your LLM generate 372 mathematical "breakthroughs" and then have 2 thousands mathematicians spend two weeks trying to understand each to tell you maybe one or two are viable...

Reply on news.ycombinator.com