A script to replicate finding of the computer assisted proof in the PolyMath 14 project is available as an executable jar here. To run this, you need to have Java 8 installed and configured to use enough memory (we used JAVA_OPTS="-Xms512m -Xmx4g"
). Assuming Java 8 is setup, the script can be run from a directory to which it is downloaded by running the following.
java -jar polymath-proof
This outputs status updates and then the proof, as well as the proof with rational coefficients. The status updates are output to the standard error, so the proof can be saved by redirecting the standard output, for example run the following.
java -jar polymath-proof > proof.md
The full source is at https://github.com/siddhartha-gadgil/Superficial. The script is generated from the object ProofScript
in the file ProofFinder.scala, from which one can trace backwards to explore how the proof in this script was generated. During the project we used the code in the file LinearNormProofs.scala instead, but this is less robust due to using more memory and garbage collection (since suboptimal proofs are constructed and discarded).
For the readers convenience, the generated output converted from markdown to html (and with unordered lists changed to ordered lists) is below. The output is a 173 line proof with double precision numbers (similar to the one originally posted) followed by the same converted to using exact (arbitrary precision) rational arithmetic.