1c211d007930cdf705501dd3e8bf749b11886a3cfcec5db005cc1f9c1899701a  paper/proof.pdf
3dfc9d6ea68aacd1a2b2d115b265abc66c69e3a3ef2d23d050c41a935e16ca2f  lean/Erdos354.lean
