Hacker News Reader

Comment by ivancho | Hacker News Reader

Their "proof" that there are only 12 solutions to 8 Mutually Non-Attacking Queens on Chessboard is just "That there are only these 12 can be proved by brute force." :/

View on HN

You have proof in sarcasm quotes, but it counts https://en.wikipedia.org/wiki/Proof_by_exhaustion

In my university math departments putnam problem competition (they'd just be on the wall, prize was a $40 giant pizza each week) they would accept the most elegant solution, so if nobody else submitted something better I'd get a pizza for just running a few lines of python.

I'm not gatekeeping proofs here, and I'm glad you got math pizza :) If proofwiki had exhaustively printed all possible arrangements, or the decision tree of constructing them, or if they had even included the code that would do the checking (like, say, https://www.richard-towers.com/2023/03/11/typescripting-the-...), then I would agree it counts. But without even a rough ballpark estimate of possible arrangements to check, asserting "brute force" does not make a proof. If I incorporate understanding of the problem, I can see that at most we need to check 8!, which is reasonable. But if the constraints were not so simple, then we might be dealing with 64-choose-8 cases instead, which is heading into not-reasonable.

They can add the same sentence under every finite fact in their wiki, but then it won't be a proof wiki, it would be a list of numeric facts they checked by brute force and we can either trust them, or check ourselves.

The task proving some statement and the task of finding the shortest, or a "reasonably short" proof, are very different endeavours.

The first is about certainty that a statement is valid ("true"). The other is about simplifying the understanding of _why_ it is valid. Most of the time, you don't care much about the latter.

It would be nice to have an reproducible example of how the result was achieved though. Otherwise it's a compendium of results, not proofs.

What is your certainty that that statement is true? What if it was a calculation which takes decades on a supercomputer?

At current rates, whatever is done on a supercomputer today is done by a cheap pocket-size device just decades later. So, I'm not too worried about this case.

One of the first famous examples of this is the four-coloring theorem. I don't know any serious mathematician who is not certain of that result.

Reply on news.ycombinator.com