This page contains an archive of the DRAT proofs generated in our resolution of Lam's problem (verifying the nonexistence of a projective plane of order ten).
There are three required cases in the verification:
- The nonexistence of codewords of weight 15
[DRAT certificate (with symmetry breaking), 34.5 MiB]
[DRAT certificate (no symmetry breaking), 438.6 MiB] - The nonexistence of codewords of weight 16
[DRAT certificates, 326.2 GiB] - The nonexistence of primitive codewords of weight 19
[DRAT certificates (A1 and A2 search), 3.3 GiB]
[DRAT certificates (complete search), 110 TiB]
The complete weight 19 certificates are not available to download due to their size. However, the weight 19 main scripts in the MathCheck2 repository will generate and verify these certificates.