Hacker News Reader

Comment by lisper | Hacker News Reader

FWIW, my assessment is that this paper passes the Aaronson test, as well as my own personal bogometer. If I were a betting man, my money would be on "the proof will turn out to have a flaw, but it will be hard to find the flaw, and the finding of the flaw will be interesting in and of itself, and possibly even advance the field."

View on HN

And even though it may be hard to find the flaw, it will be easy to verify that it is a flaw.

If only we had a way to make finding the flaw as easy as verifying the flaw

I don't think it would be possible to make finding it as easy as verifying it, but how can we prove that?

Someone should research and write a paper about it.

But then how will we know that paper is correct?

I'm pretty sure that the answer to that question involves a cat.

Sounds hard.

no problem

NP-hard.

/dodge

That was the joke. :-)

By using the algorithm!

This is getting a bit too meta for my tastes :')

Finding flaws in proofs is as easy as verifying them. After all, finding a flaw amounts to just checking a proof. Finding a proof is the truly hard challenge.

Checking a proof isn’t necessarily easy, of course, in the sense of both human hardness—such as requiring a lot of background, using dense notation, or being very long—and computational hardness, such as using a logic whose decision procedure takes exponential time.

What kind of esoteric logic yields proofs that require exponential time to check?

Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...

Well, I'm sure we can all agree that the mathematical paper we're discussing could be formalized into a proof that could be checked in linear time.

That's only obvious in a vacuous sense.

As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians:

https://mathoverflow.net/q/226966/36016

Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful.

> what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step

Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with.

EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.

Well, I've spent a lot of time with theorem provers as well as with normal mathematics. I've never experienced an exponential blowup when formalizing mathematical ideas. It would always boild down to step-by-step verification. And I don't see any reason to suspect that the paper under discussion uses non-standard techniques.

Wow, this got more replies than I expected. I was partly kidding, in that I don’t think it’s a huge concern for humans, but for example the tableau decision procedure[1] for modal logics such as epistemic logic is EXPTIME-complete[2].

[1]: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

[2]: https://arxiv.org/abs/0808.4133

My favorite comment. By far.

This lines up perfectly with most software bugs. Hard to find, but once you have them easy to prove they are the cause of the problem. The difference is that in software bugs are usually fairly easy to fix, a math proof with a bug in it might not be fixable at all.

I think you missed the joke

After overlooking the paper and applying Scott Aaronson's criterion I bet against you and bet:

- The proof will turn out to have a flaw

- The flaw will not be that hard to find (though probably not completely trivial; but rather of the kind: it takes much time to go to the details of the proof arguments)

- The flaw will not be interesting in itself and will not advance the field

Seconded. The flaws in these papers are not hard to find. They usually amount to misunderstanding of definitions or the results they cite.

Unlikely considering the author of the paper. I'm basing that on other comments on the thread which this section seems to be missing, e.g.:

> ...this guy is an established senior researcher at the University of Bonn

Even experienced people can make "silly" mistakes. https://arxiv.org/abs/1612.04208v1

They can—but that doesn't mean we should assume it's a silly mistake (as opposed to a deep one) without more information than that he's an accomplished researcher.

To add to this, I have a Ph.D. in applied mathematics. I am also an accomplished researcher, albeit retired.

I make more mistakes by 09:00 than most people will make all day. Hell, my girlfriend would suggest that we can move that time forward a couple of hours.

Reply on news.ycombinator.com