William Gasarch

Great article. Since it looks like a lot of folks are interested in this article, some extra background.

First, what is forcing? The article actually has a great description of ultrapowers (a key part of the construction) but it goes by a little fast, so you might like Tim Chow's "A beginner's guide to forcing" [1] which does a good job not only laying out the mathematical details at a high level, but also really clearly explaining the philosophy of how you prove something independent of the axioms. I found it very illuminating.

Second, the article has some interesting notes on how mathematicians go about what axioms to select and which not to. Penelope Maddy's "Believing the Axioms" [2] is the classic on this topic (it has two parts). It is focused on set theory, so it has a nice description of Martin's axiom and the arguments for and against. It was nice to read because it is a deeply technical argument (set theory is hard!) but at the same time there is no "right answer"—all of these axioms, after all, are independent of ZFC, and it's "ok" to add any of them. The arguments are sometimes aesthetic ("rules" versus "surprises"), sometimes pragmatic (what they can and cannot prove), and sometimes involve deep values of what the universe should be like (should higher cardinalities be like lower ones? weirder? simpler?).

It might all seem abstract, but if your day job is programming, imagine an argument over how to architect a large and complex system. Perhaps both…

of duck backs, water, and bridges bygone

> deterministically achievable in sub polynomial time

it's already been stated that 'sub polynomial' was a typo, the original sentence discussed subexp state of the art but i changed it to discuss my research instead and failed to remove the 'sub'

'deterministic' can also be appropriately called out as redundant when used with polynomial time because it is implied in the latter but i wanted to be explicit

> my intended inference

inference is defined as 'a conclusion reached on the basis of evidence and reasoning'

this is a word structure i use in place of faith based assumptions: i think, i believe, etc; to establish a respect for evidence based conclusions

part of my research's aim is interested in a polynomial time algo for integer factorisation, but before i am to conclude that there is such a thing i require evidence, hence it being the intended inference of my research stead a direct inference

> 'it's hard for me it must be impossible for you'

this is what you will hear very often from many in the know if you tell them you have interest in a poly factorisation algo, even in spite of the problem being open

except in the case of one of the people that fanned all this interest

Richard Karp: (Berkeley, unsure, P=/=NP) My intuitive belief is that P is unequal to NP,
but the only supporting arguments I can offer are the failure of all efforts to place specific
NP-complete problems in P by constructing…

This is a great question that permeates all verification work. In the lingo, we call the set of assumptions a proof makes the "trusted computing base" (see https://en.wikipedia.org/wiki/Trusted_computing_base ).

I listed some of the assumptions we made in another comment https://news.ycombinator.com/item?id=10018985 .

The question you ask was believed for a long time to be the death knell of formal verification. It was persuasively argued in "Social Processes and Proofs of Theorems and Programs" https://www.cs.umd.edu/~gasarch/BLOGPAPERS/social.pdf that any proof of a complex system is necessarily at least as complex. Thus there would be no reason to trust the proof any more than the original code.

The breakthrough in verification came when we started using machine-checked proofs. In this approach, you write a short, simple, and trusted proof checker. You can then verify complex systems using complex proofs that are checked by the simple checker. Then the only possible errors in the proof can come from the proof checker being wrong. Because the checker is simple and general (ie, it can check all kinds of proofs, not just proofs about a particular program), it is more trustworthy.

Just to reiterate (including some content from my other comment): we can be wrong only if we have written the wrong definition of linearizability, misstated the correctness theorem, or if there is a bug in the proof checker or in Coq's logic itself.

There is a section that uses the same type of thinking that you can use to prove the R(3, 3) = 6 case (often known as the Theorem of Friends and Strangers [0]), towards the end of the paper [1] (though in a pretty different way). Proving the general case of things is often very removed from the proofs of a specific case, so its interesting to see similar thinking in the general case.

Also, I really like the simplicity of the proof of the Theorem of Friends and Strangers. You can show someone the proof with two colored pens in 10 minutes. But at the same time, it uses some interesting proof tools: contradiction, the pidgeonhole principle, creating a boundary by counterexample (ie that R(3, 3) must be greater than 5). So I like the Friends and Strangers proof for its elegance and how fun it is to show people, and I like Ramsey's proof because it captures some of the fun of the R(3, 3) case while proving something much, much more difficult.

[0] https://en.wikipedia.org/wiki/Theorem_on_friends_and_strangers

[1] https://www.cs.umd.edu/~gasarch/BLOGPAPERS/ramseyorig.pdf

I've placed 74 using an IP solver

1 1 . . . . . 1 1 . . . . . 1 . .
. 1 1 1 1 . . . . . . . . . . . .
1 . 1 . . 1 . . . . . 1 . . . . 1
1 . . 1 . . 1 . . . 1 . . . . 1 .
1 . . . 1 . . . . 1 . . . 1 . . .
. . . 1 . 1 . 1 . . . . . 1 . . .
. 1 . . . 1 1 . . 1 . . . . . . .
. . 1 . . . 1 1 . . . . 1 . . . .
. . . . 1 1 . . 1 . . . 1 . . 1 .
. . 1 . . . . . 1 1 1 . . . . . .
. . . . 1 . . 1 . . 1 1 . . . . .
. . . . . . 1 . 1 . . 1 . 1 . . .
. . . 1 . . . . . 1 . 1 1 . 1 . .
. 1 . . . . . . . . 1 . 1 1 . . 1
. . 1 . . . . . . . . . . 1 1 1 .
. . . . 1 . 1 . . . . . . . 1 . 1
. . . . . . . 1 . 1 . . . . . 1 1

The solver chokes on anything larger than a 6x6 grid, but I've had good luck adding one row at a time to a smaller solution.

http://pastebin.com/m4c4696af

edit: He mentions that he already found a size 74 set in one of the linked pdfs.
http://www.cs.umd.edu/~gasarch/BLOGPAPERS/17x17.pdf

Tang is smart, but the author of this piece is unfairly characterizing Aaronson's beliefs and the nature of the P=NP problem.

I don't know a single mathematician or computer scientist researcher that thinks that P=NP is likely. I know they exist, based on this poll[0], but in practice P equaling NP would be incredibly surprising. And even if it does somehow, I highly doubt the equality would practically hold.

The reason I think it is fair for Aaronson to operate as if P!=NP is that even if it is unproven, it doesn't mean we can't make judgements about its relative likelihood. I haven't proven that all beetles are slower than the fastest cheetah, but based on what I understand about cheetahs and beetles I can operate as if I do and change my mind if I'm proven wrong. I think it's less likely that P=NP than it is that a beetle can outrace a cheetah.

[0] http://www.cs.umd.edu/~gasarch/papers/poll2012.pdf