|
|
|
|
|
|
by Someone
2122 days ago
|
|
|
Paper is at https://arxiv.org/abs/1910.03740. Skimming it the answer appears to be “because they had that cluster”. They say they only used 20 machines (each with 24 CPUs, so I guess these are fairly beefy) Given the 224 GB (binary) size of the proof memory usage might be a problem, too. |
|
|