Hacker News Reader

Comment by ijustlovemath | Hacker News Reader

I also don't think there's been nearly enough time for peer review of what was actually formalized vs what was intended. How many humans out there actually have a deep enough understanding of the background to be able to check the work? I understand that Lean checks the mechanical steps, but if it's building a ladder to some other result entirely, nobody (certainly nobody on HN) will know for some time.

I'm probably wrong, but what's the point of throwing away all skepticism?

View on HN

You only need the problem statement to be correct in Lean, no matter what route it goes down is correct as long as the original formalization of the problem is correct, which is substantially easier to check. Not sure how many people have checked that so far, but I'm guessing the math community would be quick to point out if something basic like that was missed for something like a new bound on RH.

Nothing wrong with being skeptical, but I see no reason to be skeptical as of yet.

Were days out, the default should probably be skepticism for about a decade.

There's nothing to check there, they used the standard mathlib implementation of RH. THey didn't write their own for the 7/8ths proof.

Is Lean so bullet-proof that it never has soundness problems? Something LLM can exploit deep down without anyone noticing.

Recently a lean formalized proof of the Collatz conjecture had exploited bugs in the lean kernel. However, the kernel is fairly small so hopefully it'll be bullet proof soonish.

It should be noted that it wasn't a legitimate attempt at the collatz conjecture. Someone found a lean bug and created the proof to show it off. It wasn't an llm reward hacking (but this still is a concerning risk). Lean probably isn't the best kernel for adversarial proofs, but it probably has too much momentum at this point for anything else to take over.

I’m curious if ACL2 is in the running

They should use LLM to verify/prove Lean soundness first before working on something that relies on Lean.

"Chain of soundness" i think.

Apparently "only" needing the problem statement to be correct (i.e. expressing/rewriting a mathematical proof in Lean) isn't so simple, and if you don't get it correct then you haven't proved (or disproved) what you were intending.

The huggingface hack is a reason to be skeptical. Thats a pretty clear instance of a misaligned model and the models are undeniably very good at this point. Meaning also good enough to reward hack by finding and exploiting holes in lean or adversarially formalizing the problem in ways that are deliberately subtly wrong in ways that are hard to check but result in formalizing a problem that's easier to solve. There are pretty strong incentives (hype for IPO) for creating conditions that drive that kind of misalignment

If it's anything like programming, then LLMs are still worse than the best developers. If you give them any freedom then they choose worse solutions than what's possible by any metric about 50% of the time. If they don't need to invent anything at all, they are great, otherwise they are bad. The only metric in which they are better is speed. For example the other day I used Claude for an anti accidental double clicking mechanism on Android Compose. I even listed, and give examples what it should do, what shouldn't, and I give the freedom to choose an exact solution (it's a very simple problem). About half of the code wasn't needed. And some of them caused real problems. Also its solution was far from good. It was error prone as hell. For some reasons it didn't handle at the point where clickability is defined, but one layer up with more boilerplate than it needs... which is not great at all. They also cannot handle flows well at all. It works for PoC, and for quick tests, and nothing for any complexity even a little bit, like having the same screen twice on the stack. But of course, if it has an example, how it should be done, then it copies the logic well.. Also we vibe coded a website recently. There were a ton of bugs on the happy path, which were considered finished by its creator. I don't even want to imagine what's with error cases, which I'm quite sure nobody tested.

Good question whether Lean is enough.

Again, you don't need to check the proof, Lean does that. You need to check the statement, which is a much easier task. So yes, you are wrong. Skepticism is good, but it is usually just ignorance.

It's surprisingly easy to prove something subtly different than you intend actually. Digesting and understanding a theorem statement can often take significant time and expertise.

What a bizarre take. Skepticism is usually ignorance!?

The should be on AI labs to definitively prove their extraordinary claims, and they should be paying mathematicians to do so given that the results from these machines are so opaque and often nonsensical.

Incredible, your very own ignorance is showing through in your derision of skepticism as ignorance.

LLMs are very good now - meaning you do actually need to check the proof to make sure a misaligned agent didn't reward hack by exploiting some issue in lean or adversarially incorrectly formalize the statement in a way that's subtly wrong and easy to miss when you're trying to dump 75 trillion proofs on the Internet to drive hype that also makes the proof easier to solve. Probably also something you can use ai to help with though - I'm sure the other lab is having a bunch of llms adversarially review all these proofs since finding issues hypes _their_ IPO cycle. As the software world is learning - don't review ai code until a different ai has reviewed it lol.

Reply on news.ycombinator.com