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
[DRAT certificate (with symmetry breaking), 34.5 MiB]
[ (no symmetry breaking), 438.6 MiB] - The nonexistence of codewords of weight 16
[, 326.2 GiB] - The nonexistence of primitive codewords of weight 19
[ (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 in the MathCheck2 repository will generate and verify these certificates.