Projective plane proofs

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:

  1. The nonexistence of codewords of weight 15
    [DRAT certificate (with symmetry breaking), 34.5 MiB]
    [DRAT certificate (no symmetry breaking), 438.6 MiB]
  2. The nonexistence of codewords of weight 16
    [DRAT certificates, 326.2 GiB]
  3. 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.