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."

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?

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

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. :-)

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

By using the algorithm!

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.

"Yet here’s the bloodied patient, and here we are in the emergency room." "The lemma encrusted shoulders of giants."

Aaronson on writes very well.

"At some point, there might be nothing left to do except to roll up your sleeves, brew some coffee, and tell your graduate student to read the paper and report back to you."

I'd rather he applied his test to a bunch of papers for validation and showed us a confusion matrix.

A little too flowery. He's also needlessly political.

Are you one of those people who equates any mention whatsoever of Trump as "being needlessly political"?

No, but this one was.

Could you clarify what was needlessly political? I can't seem to find anything political there at all.

Injecting a controversial (and mostly detested here) political figure into an unrelated topic.

I meant actual examples. But on second read I assume this is about the blog in general and not this post in particular that doesn't seem to have any Trump references.

Not at all. But bringing him up in an unrelated post on a technical blog just screams "virtue signaling" to me.

When you feel strongly about something and write about it, you aren't virtue signalling, you're expressing your view. If you have any reason to take the rather uncharitable stance that his views on Trump are inauthentic, then post them, otherwise it's better just to assume that people who say things you disagree with actually think those things rather than are just saying them to look good.

Accusing others of "virtue signaling" is a much clearer example of "virtue signaling" in my opinion, since it's a particular population that tends to do it, and is used primarily to put down those they disagree with and mark them as belonging to a different group rather than to actually make any kind of meaningful point.

I'm curious what I said that sounded to you like "his stated views on Trump aren't authentic."

https://en.wikipedia.org/wiki/Virtue_signalling

    Virtue signalling is the conspicuous expression of moral
    values done primarily with the intent of enhancing
    standing within a social group.

I don't think Aaronson states his views on Trump with the hopes of increasing his social status. He does it because it's just what he feels and wants to express himself.

And which part of that definition has anything to do with the views being inauthentic?

I feel like I'm taking crazy pills here.

When you express a view that you don't hold in order to receive social approval, or when you express a view that you hold lightly with more intensity and frequency than you would except for your desire to receive social approval you are being inauthentic.

The whole value of the phrase 'virtue signalling' is that it accuses those you disagree with of inauthenticity. If I'm saying a thing I genuinely believe because I genuinely believe it, I'm not virtue signalling. It's only if the reason for saying the thing is to gain social approval that it's 'virtue signalling'. Any assumption that your opponent is doing something for this reason is uncharitable, and kills rational debate. It's essentially an ad hominem attack.

It's also ignoring the fairly detailed entry that Scott posted explaining in his own words why he started talking about Trump in his blog: http://www.scottaaronson.com/blog/?p=2777 when previously he'd avoided the subject.

Maybe it is virtue signalling, or maybe he really did feel as he claimed, that he had a moral responsibility to speak out against Trump. If you assume that it is only 'virtue signalling', you are cutting yourself off from engaging with his points.

You're correct.

Virtue signalling is usually done by people who sincerely believe the values they espouse - but they emphasize or show those values in order to gain or reinforce social status within the group. It usually is done by proclaiming things you hate, rather than things you like.

If the comment adds nothing besides an "I'm with you guys, that's the worst", it's fair to see and describe it as virtue signalling.

And yes, it happens on both sides of the aisle - heard lots of conservatives proclaiming their distaste for Obama over the last decade.

>virtue signaling

You know that was an interesting and useful concept before you guys decided to turn into yet another empty insult to fling at people.

It's still an interesting and useful concept even if it's also used as an insult. (Much like you might refer to a colleague's tight new shirt and gold chain as a "mating display" without disparaging biologists' use of the term.)

I mean he also pokes fun at his children, himself, and posted a rap video about theoretical computer science on his blog. His blog is not exactly the Annals here... I think he is more than welcome to write about whatever he damn pleases and if you disagree you are more than welcome to argue in his comment sections (and more than likely lose)

Of course he's welcome to write about whatever he likes. It's his blog.

But I'm welcome to roll my eyes at it.

I'm rolling my eyes at your eye rolling! How deep can we go?!

In what world is Scott Aaronson, a professor whose primary research area is computational complexity, unrelated to a P=NP solution?

I was saying that President Trump is unrelated to the usual topics on that blog.

Proof for the Gaussian correlation inequality was

- Written in Word

- Uses techniques just seem too wimpy for the problem at hand.

- Was published in a predatory journal

For those curious about the details of this, I found this interesting article: https://www.quantamagazine.org/statistician-proves-gaussian-....

Hence why Scott explicitly takes time to address that there will surely be outliers on both ends

I just wanted to point out that's is not a theoretical possibility, but actual ground breaking work did look sketchy as hell.

The "The nice thing about math is that sooner or later the truth comes out" bothers me. The knowlege in Archimedes palimpsest was lost so long the eventually doesn't seem to be much comfort.

Grassman was another more recent example, though obviously we can't now find recent examples that will lie dormant for millennia...

When we trust Academia to write their own history books, the theme is always "sooner or later the truth comes out."

See also the more P-vs-NP specific version he put out later: http://www.scottaaronson.com/blog/?p=458

"At some point, there might be nothing left to do except to roll up your sleeves, brew some coffee, and tell your graduate student to read the paper and report back to you."

So there's your real answer.

Aaronson has commented on this particular proof. He's, to say the least, skeptical, based on an observed polynomial circuit in section 7: http://www.scottaaronson.com/blog/?p=3389

Points number 6 and 10 may apply. I only skimmed the paper and may have missed the really interesting point, but to me the argument and method just looks too simple to have been missed by everyone for all the time. But I am also totally not an expert in the field.

Aarsonson has since commented on this paper on his website. He still believes that it's a bogus proof.

The question is, how can you do it in polynomial time? :)