[ivancho]

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.