This conjecture was originally proved in 2016 by Marijn J.H. Heule, Oliver Kullmann, and Victor Marek. Details on their proof and all their data is available from their web site
We formalized all elements of the original proof in the Coq theorem prover: the original SAT encoding, the simplified SAT encoding, the cube-and-conquer parallelization of the proof, and the unsatisfiability of the resulting 1,000,001 formulas.
You can download a journal article (submitted to JAR), the formalization, and the generated documentation (or browse the documentation online). The article builds on two conference papers, one regarding the encoding (to be presented at LPAR-21) and one regarding the unsatisfiability checking (to be presented at TACAS 2017).
In order to check the proof, two checkers are extracted by executing make from the formalization: one for checking that the disjunction of the cubes forms a tautology and one for checking that the conjunctions of the individual cubes with the simplified generated formula are unsatisfiable. (A third general checker for unsatisfiability proofs can be obtained by executing make checker, if one desires to check other proofs of unsatisfiability.)
To check the full proof of the Boolean Pythagorean Triples problem, first the tautology has to be checked by executing make tautology. Then, for each of the 1,000 sets of 1,000 cubes each, their unsatisfiability proofs are reinstantiated and checked by executing: for i in $(seq 0 999); do make cubes/$i; done
We used OCaml 4.01.0 and Coq 8.5pl3 for the proofs. We tested the checkers and scripts also with OCaml 4.04.0 and Coq 8.6. We ran the proofs on Ubuntu, centOS, and macOS Sierra. (On macOS we installed coq, ocaml, ocamlbuild, and opam using Homebrew.)
WARNING 1: Executing make tautology and make cubes/$i will download nearly 70 GB of data from the web site of the original proof.
WARNING 2: Preparing and checking each set of 1,000 cubes by executing make cubes/$i will require around 500 GB of free diskspace. The total size of all proof files produced is around 400 TB.
WARNING 3: Executing make cubes/$i will use all logical cores in preparing the 1,000 proof files, but only one core for checking them. If you plan on actually running all 1,000 cubes, you are advised to split the preparation (calling prepare.sh $i) and the checking (calling e.g. InterfaceCubes.native million.cubes $((i*1000+1)) $((i*1000+500)) and InterfaceCubes.native million.cubes $((i*1000+501)) $((i*1000+1000)) in order to distribute the load to two or more cores). Alternatively, you might first run all preparations in parallel on several nodes and then several checkers in parallel on one node.