The Boolean Pythagorean Triples problem asks the following question:
Is it possible to partition the positive integers into two sets such that no set contains a Pythagorean triple (three numbers a, b and c with a^2 + b^2 = c^2)?
In 2016, Marijn J.H. Heule proved via computer search that the integers up to 7824 can be partitioned this way, but it is impossible to partition the integers up to 7825, thus resolving this as NO.
The first part can be trivially demonstrated by listing the partition, but there is no easy way to show the absence of a partition for the numbers up to 7825. The proof consisted of a summary of the steps taken by the exhaustive computer search, and thus was over 200tb in size, dubbed "the largest proof in the world" at the time.
Obviously, a brute-force computer proof like this is not satisfying. Will a concise, human readable proof for this problem be published by the end of 2025? It doesn't have to specifically be limited to 7825. If someone finds a simple proof that the integers up to 10^10^10 can't be partitioned, that would still count.
1,000
3.00there is no easy way to show the absence of a partition for the numbers up to 7825
Huh. Is there a proof that there is no "easy way"?
The obvious easy way: reduce the set to a small subset that is not partitionable. If instead of Pythagorean Triples, we ask about some other property P of triples, you could show that a large set is unpartitionable by exhibiting a subset of five elements such that any triple drawn from that set exhibits the property P.
So then the question becomes: how small can a minimal subset be? The proof demonstrates a bound of 7825, but this is clearly not the lower bound... the subset [3 .. 7825] is presumably also not partitionable since 1 and 2 don't participate in any triples at all, the smallest being 3,4,5. I suspect some work would rapidly raise the minimum size of an unpartitionable set beyond size 5.
So one awkward question is: how small would a brute-force proof of a subset have to be to count as human readable?
Obviously this market is hoping for a nicer proof than that.
If the minimum size of an unpartitionable set is large, comparable to the 7825 example proven, then it seems plausible that improving on the ugly SAT-solver mess is difficult.
Anyway, thanks for posting this, that's an interesting problem to ponder.
@EvanDaniel There's no known easy way. Obviously if it were proved that there's no simple proof, the market could already be resolved NO.
As for what the exact threshold of "human readable" is, I'm not sure of a good way to operationalize it, but I think it is unlikely to matter. But I guess if you want an upper bound on case analysis, how about "500kb of text as expressed in natural English with enough comments to easily follow the logic". Does that seem reasonable?
@EvanDaniel My expectation is that if you confine yourself to small integers, 7825 is minimal (once you've done the obvious simplifications like excluding numbers that are only present in one triple, and removing an element from each magic square, which gets you down to around 3200, IIRC)
You might be able to find a smaller minimal set by choosing large integers with a special pattern, but I'm not optimistic.
@ThisProfileDoesntExist I'm not actually that worried about specifying it better. "I know it when I see it" seems like it will be fine on this one. Mostly I was just thinking out loud about how one might try to simplify the existing proof and noticed the possible weird result.
Proof of no simple proof would itself be fascinating. I was pondering the narrower question of "proof of no simple proof using this specific proof strategy". That seems like it might be tractable.
@EvanDaniel There are exponential lower bounds on the minimum length of a resolution proof (the kind that SAT solvers produce) for certain problems, but I don't think anyone's tried to prove that for this problem, and in any case, that would say nothing about the possibility of a short higher level proof.
E.g. if you try to prove the pigeonhole principle using the same techniques used here, the minimum possible proof length is O(2^sqrt(n)), but there's a very trivial non-resolution proof of the theorem.