Certificate, programs and Lean formalization for "A lower bound for Moser's worm problem with rotations and translations"

Certificate, programs and formal proofs for the paper A lower bound for Moser's worm problem with rotations and translations (doi:10.5281/zenodo.23717800), which proves that every convex set in the plane that contains a rotated and translated copy of every arc of length 1 has area at least 0.2414. This is constant 13a in Tao et al.'s repository of optimization constants, the version in which reflections are not allowed. The record holds two formal proofs of this bound in Lean 4, each with its data: a compiled-code proof, which relies on code generated by Lean's compiler, and a kernel-only proof, which the Lean kernel checks without such code. From version 7 the paper, the README, the citation file and this description changed, and the repository now also holds the LaTeX source of the paper; the certificate, the programs and the Lean files are the same. Files. The certificate, 433,912,890 leaves in 16,384 parts, in nineteen archives of at most 0.9 GB (9.9 GB in total). Each archive holds a contiguous range of parts and a list MANIFEST_K.txt of the SHA-256 hashes of their files, so that it can be checked on its own: cert_w2414a_0.tar (96,000,000 bytes, SHA-256 b1a5da03eb3d8a33d9ec618b218c9389221ffca8db9a066efb9de1ced103b809) cert_w2414a_1.tar (894,320,640 bytes, SHA-256 dd572fa41e11e8090a198e017f03dee0961705761ad13f514e8cb4c6afe6ed2d) cert_w2414a_2.tar (168,949,760 bytes, SHA-256 13119f985313a77ab7a8701f5a20e8127f71d774a428f0237b140ce31c411aba) cert_w2414a_3.tar (596,910,080 bytes, SHA-256 da3447a77960cc9d78f8fc1a593b76d0f7efb58853c723830a0a9cee8a503853) cert_w2414a_4.tar (389,939,200 bytes, SHA-256 3137f59c2eb7176b87eb3cb6d34c43c54cca0c943ad352d81f862ca811dc69f7) cert_w2414a_5.tar (875,376,640 bytes, SHA-256 ab7ac37c7b205a51c655cd59df6bd749e6519b7e86bb75b4a2a3ee482381d48b) cert_w2414a_6.tar (589,178,880 bytes, SHA-256 df7f08302cb95243d35d95c7bca82e40b092f431c1bc370db28f39c2df4a0d9a) cert_w2414a_7.tar (245,565,440 bytes, SHA-256 23eb4aed2f901b4cbc31bb798b0740d64b733c578549ab3a48a066a381caca49) cert_w2414a_8.tar (538,296,320 bytes, SHA-256 4d3d7b2e60fce8b33155eedf2e058c94b9557eb0a09b5553fa3a8be75c51b3b5) cert_w2414a_9.tar (538,357,760 bytes, SHA-256 dfe48bd77979e29eef4de52d425f128553623d1a30302c10dabd26e8fd55d8e2) cert_w2414a_10.tar (598,937,600 bytes, SHA-256 b1e91658c695fe50a200b0c90d2ef3b74f340a3710132fa8814eb42e9d5f7fea) cert_w2414a_11.tar (594,083,840 bytes, SHA-256 1d9cb8a47e14b8ae55ec85c184b7feb6398870b3f0ef597f6fafb2ca55fcabe3) cert_w2414a_12.tar (603,228,160 bytes, SHA-256 58dcf7e275f9143e8b63322e7e5c25b4b402e7ba05804d3cb28a86982a155d20) cert_w2414a_13.tar (450,734,080 bytes, SHA-256 b362975cda6c82ceeaa400a3b34a2a9f732e352e707ae3b00bd108fbc2dc497e) cert_w2414a_14.tar (603,996,160 bytes, SHA-256 b3a73656e0721009594b1ef127b75a0cedac06374383efba2c39d545d4ee8e1a) cert_w2414a_15.tar (607,037,440 bytes, SHA-256 d20e1bdceb8cfaf84798f6327ff0f4ba1708995875b1a81e4afa8e87d6035cab) cert_w2414a_16.tar (595,087,360 bytes, SHA-256 6229c0d33ac01d219d461aa90c50e978739d3b4ee426102af730be0ccede9a01) cert_w2414a_17.tar (416,317,440 bytes, SHA-256 caa18ba0b091760261de62a630522b597c1e17f00d0006936b04f8dfccc69b69) cert_w2414a_18.tar (493,332,480 bytes, SHA-256 48e4e512322026a7dec3c00d4ad13e6d31ec159a3859a6a44d151b11e01377cc) The data of the compiled-code proof: the certificate converted into text (18.5 GB), in seven zstd-compressed tar archives (7.33 GB in total). Extracted into the directory lean/ of the zip file, they create lean/data/, whose files are listed with their SHA-256 hashes in data/SHA256SUMS: worm_data_2414_meta.tar.zst (1,486,125 bytes, SHA-256 0b96db545c6e01e0efa384981355f42fd109445ca852247fa9a76f51ed64d4a0): the skeletons of the 16,384 parts, manifest.json and SHA256SUMS worm_data_2414_chunks1.tar.zst (1,186,415,124 bytes, SHA-256 415ab4cca690d8f389acd7d19a11ed1a195e73f98052bac8269f8e265ca45aa4): chunks 0 to 1779 worm_data_2414_chunks2.tar.zst (1,218,571,276 bytes, SHA-256 2ded84821ee10d66e856ca85966b186e45da21d5306ce5ce53e79fd7316ebc43): chunks 1780 to 3598 worm_data_2414_chunks3.tar.zst (1,210,622,103 bytes, SHA-256 1a9de88f49919c0f448ec828958a3715b2abdb0f9a981d6ecf8d5e525e209ec5): chunks 3599 to 5336 worm_data_2414_chunks4.tar.zst (1,234,882,437 bytes, SHA-256 16af22e7dce9de98cf112e133001087ba9197b704c0023724716c8d87be86c8f): chunks 5337 to 7215 worm_data_2414_chunks5.tar.zst (1,238,068,119 bytes, SHA-256 de01529626083e768ead14e73ca551ae4e9f49fa11bec0ae3690c7aec3f899da): chunks 7216 to 9183 worm_data_2414_chunks6.tar.zst (1,241,062,543 bytes, SHA-256 3893c7f893eee074f4ff0e773bbd300357c1fce1c84215ddac1d7ef502d385d9): chunks 9184 to 11071 The data of the kernel-only proof, in two archives split into zstd-compressed tar parts of at most 2 GB (14.12 GB in total). Each part is a complete tar file; the parts of an archive are extracted into the same directory: the Lean project of this proof, that is, the directory lean_k/ of the zip file together with the 261,772 generated modules, in six parts: worm_k2414_sources_part1of6.tar.zst (713,480,436 bytes, SHA-256 991cfd0538376d340a760d485e27a5f57adabb24e8fc3534f9fbf3f39d6e8cb5) worm_k2414_sources_part2of6.tar.zst (704,187,804 bytes, SHA-256 287d3a7b7ae1e2436933641bc1687163544fb45b11bd7298e3401aac1e0ab640) worm_k2414_sources_part3of6.tar.zst (1,716,476,810 bytes, SHA-256 3f716ce7b6c7a8dd8ac8f4f5bc88b900c2664c723a682babf5f574ae7d1a0c51) worm_k2414_sources_part4of6.tar.zst (1,708,046,779 bytes, SHA-256 0a436951cd1bdfb9294b07c89da2349947a25f8a6b45d5050e0f6e75e612a973) worm_k2414_sources_part5of6.tar.zst (1,674,633,637 bytes, SHA-256 b392e38125452f312a66fbfe3aac71e07edb769ca8cd1b47179967becd2720c9) worm_k2414_sources_part6of6.tar.zst (824,121,027 bytes, SHA-256 620a8441b735a3295ff0218f6c0c9fadd2a5a5d13f8e16db9c4429f44984edd8) the merged certificate in 11,072 chunks, with the skeletons and the family file from which the generator writes the modules, in four parts: worm_k2414_merged_certificate_part1of4.tar.zst (1,727,337,217 bytes, SHA-256 b4044b2b6a142de802682816dabd6498fba5be96b73e3b7f3cdfa7bae54f8fb3) worm_k2414_merged_certificate_part2of4.tar.zst (1,739,691,014 bytes, SHA-256 29bccb27af875be58ab5756da2f9bd3667c756b39e144b59668c2d484877ce54) worm_k2414_merged_certificate_part3of4.tar.zst (1,777,428,415 bytes, SHA-256 2ec65bd3a152da3399f288531ffa123e7615d4469f897e9aa4d90a0348ea6e28) worm_k2414_merged_certificate_part4of4.tar.zst (1,530,117,941 bytes, SHA-256 e6b3b702fabb270a37a6bf800f533ce121b255851ab658bfb22ea5b3dfd45175) SHA256SUMS: checksums for the archives and the zip file. moser-worm-rotations-bound-83604e287a33.zip: the checker, the programs that check the headers and the coverage of the leaves, the tests, the results of all check runs, the search programs, the paper's data and the Lean files, identical to the GitHub repository github.com/tejasvi/moser-worm-rotations-bound/tree/v8 at commit 83604e287a33dc81d6aaaa104f209896a4e8ac90. Checking. The checker needs Python 3 with numpy and python-flint. The README in the zip gives the commands and the range of parts in each archive. Repeating all the check runs took 208 CPU-hours; a CPU-hour is an hour of one hardware thread (virtual CPU) of a cloud server. The compiled-code proof needs Lean 4 (version 4.35.0-rc3) with Mathlib; lean/README.md gives the commands. Compiling its chunk modules took about 680 CPU-hours. The kernel-only proof uses the same Lean version; lean_k/README.md gives its commands, and checking its modules took about 29,000 CPU-hours. Version 4 of this record, doi:10.5281/zenodo.23557869, holds the certificate for the bound 0.241, from which the search for the certificate in this record started, together with the data of a compiled-code Lean proof of that bound. A kernel-only proof of the weaker bound 0.241, with the archives of its data, is in version 6, doi:10.5281/zenodo.23585570; one of the weaker bound 0.24 is in versions 4 and 5, doi:10.5281/zenodo.23557869 and doi:10.5281/zenodo.23574657.