Two-hundred-terabyte math proof is largest ever

Darn, I had no idea one could get into the media with this kind of stuff.<p>I had a much larger &quot;proof&quot;, where we didn&#x27;t bother storing all the details, in which we enumerated 718,981,858,383,872 semigroups, towards counting the semigroups of size 10.<p>Uncompressed, it would have been about 63,000 terabytes just for the semigroups, and about a thousand times that to store the &quot;proof&quot;, which is just the tree of the search.<p>Of course, it would have compressed <i>extremely</i> well, but also I&#x27;m not sure it would have had any value, you could rebuild the search tree much faster than you could read it from a disc, and if anyone re-verified our calculation I would prefer they did it by a slightly different search, which would give us much better guarantees of correctness.

Probably the code used to generate the 200TB was not 200TB itself, right?<p>So in a sense, the code is the proof, and the 200TB is just something it generates as a side effect.

There is an increasing appreciation that large proofs need &quot;proof engineering&quot; that is similar to software engineering. See e.g.<p>- D. Aspinall, C. Kaliszyk, Towards Formal Proof Metrics.<p>- G. Klein, Proof Engineering Considered Essential.<p>- G. Gonthier, Engineering Mathematics: The Odd Order Theorem Proof.<p>- T. Bourke, M. Daum, G. Klein, R. Kolanski, Challenges and Experiences in Managing Large-Scale Proofs.

A relevant article on large proofs: <a href="http:&#x2F;&#x2F;gallium.inria.fr&#x2F;blog&#x2F;large-proofs&#x2F;" rel="nofollow">http:&#x2F;&#x2F;gallium.inria.fr&#x2F;blog&#x2F;large-proofs&#x2F;</a>

&quot;but when you reach 7,825, it is impossible for every Pythagorean triple to be multicoloured&quot;<p>So they didn&#x27;t know in advance how long it was going to take or the size of the output?

I think &quot;brute force math&quot; would be a good name for this technique --- that diagram reminds me of finding hash collisions:<p><a href="http:&#x2F;&#x2F;www.links.org&#x2F;?p=6" rel="nofollow">http:&#x2F;&#x2F;www.links.org&#x2F;?p=6</a>

Is the data compressed and piped into a known compression algorithm, or is there some other technique used? I&#x27;d love to know how the actual program is run. Side note... the visual output is really interesting to see, and I&#x27;ll admit I crossed my eyes at it to see if I could see some sort of pattern (read: there was no sailboat).

&gt; <i>Although the computer solution has cracked the Boolean Pythagorean triples problem, it hasn’t provided an underlying reason why the colouring is impossible, or explored whether the number 7,825 is meaningful, says Kullmann.</i><p>Kind of reminds me of why we were always taught to avoid proof by induction (the mathematical kind[0]) when possible.<p>Also, funny coincidence, but the shortest math paper published in a serious journal[1] was also a &quot;no insight into <i>why</i>&quot; kind of proof.<p>[0] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Mathematical_induction" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Mathematical_induction</a><p>[1] <a href="http:&#x2F;&#x2F;www.openculture.com&#x2F;2015&#x2F;04&#x2F;shortest-known-paper-in-a-serious-math-journal.html" rel="nofollow">http:&#x2F;&#x2F;www.openculture.com&#x2F;2015&#x2F;04&#x2F;shortest-known-paper-in-a...</a>

If you verified the code performed the correct function, ensured it ran correctly and computed the result, then the code itself serves as most of the proof (not the 200TB). Really what you want to be peer-reviewed is the code, not the swathes of data.

Surely the value of this is that it provides a counterexample to a long-standing conjecture. The proof that it is a counterexample may not be too enlightening, but that&#x27;s hardly the point.

This isn&#x27;t mathematics, this is data analysis.<p>A mathematician doesn&#x27;t come up with a research where he says: &quot;Ei look, we are now extremely confident that this theorem applies in every case... we don&#x27;t have a full mathematical proof for it but I can show you all these cases where it holds true.&quot;<p>No, a mathematician proposes a result and then goes on to prove or disprove mathematically that it holds true under specific conditions in absolutely every case where those conditions are met.

I have discovered a truly marvelous demonstration of this proposition that this margin is too narrow to contain.