Certificates: the record set for k=4 (Erdős #169)

The stage table, the computation scripts and the Lean sources (the lemma, and the theorem about the set itself) used in "The record for k=4 has moved too" in the article on the Erdős conjecture on arithmetic progressions. The stage table is plain text containing only integers; its internal consistency, and the fact that it beats the record, can be checked with the Python standard library alone. That the set is 4-AP-free and its reciprocal sum beats the record is a theorem in Lean 4. 日本語版：証明書（日本語）.

The claim: there is an explicit finite set A containing no four-term arithmetic progression whose reciprocal sum exceeds 4.439753474215620 (a Lean 4 theorem, Shiori1112.setA4_apfree_and_lower). Exact integer evaluation places the sum in [4.439753474496394, 4.439753474534855]. Hence f(4) ≥ 4.4397534742. Walker's (2025) record set K(S,55)+1 has reciprocal sum 4.439753369254540 (his 4.43975 is a truncation); the Lean bound alone beats it by +1.05×10⁻⁷.

Files

To check it in Lean, start with this one file. A self-contained verification environment: the k=3 distribution (74 files) with the 19 k=4 files on top. Unpack it and run ./verify-k4.sh; it builds one file at a time and ends with the #print axioms of the main theorem.

Full sha256: shioriproofs-k4-src.tar.gz = c00cd1559181f1c555bb7974a594d0734348faf59eccc1c758c0889b29620972. The k=3 distribution (shioriproofs-src.tar.gz) is unchanged; this archive contains it.

Individual files

The table, the scripts and the Lean files one by one. The Lean files are the same as those inside the archive above.

Full sha256: f4-stages-38.txt = f7685f6524e86bacfd24346eee8465aa8680c09e2f31bd3728314574d74b5abc; check_f4_stages.py = d40067ae5992f54c93b63b1390fdabf48494a32c5ec437741775e7cfe47dbe29; erdos1110f4.py = 3f226d89fbf2333cbdb91b0d70d7d1f3ee3737821acc3395f3c28af880d0f07f; erdos1111f4.py = 06408deeb1f42fad7cb61054b0de0a830967a4396bc59bd0b863dda02781189f; erdos834.py = cd75ff9b6b4dd551f88d055264dc35fe709b74384c5a17953d15c60ef3434b02; erdos775-maxelt.txt = 69fdd457af36a04ed1e8a04d4f470842149d39ddd4c770e941f9f326b5ee57ec; Erdos1109.lean = d64492ceef990e8052f737eba56aeea57750087e3b02c4684f8ac4d26f48ec21; Chk1109.lean = 48e04f60a3090d26e18054b1ab9d0acdd51a129644ca68242025c8c6e1ab6754

In the three Python files, only the places that pointed to absolute paths on the author's machine (the import search path and the location of the reference table) were changed to paths relative to this directory. The computation is unchanged. The changed lines are marked "changed for distribution".

Lean for the set itself (the main theorem)

The lemma applied to the 38-stage construction, together with the 4-AP-freeness of the head and the lower bound on the reciprocal sum, closed for the set itself. namespace Shiori1112.

theorem setA4_apfree_and_beats_walker :
    APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
      (4439753369254541 : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x

theorem setA4_apfree_and_lower :
    APFreeK 4 {x : ℤ | ∃ n ∈ setA4, x = (n : ℤ)} ∧
      (4439753474215620 : ℚ) / 10 ^ 15 < ∑ x ∈ setA4, (1 : ℚ) / x

Full sha256: Erdos1112h.lean = 4f351de54f6bce7283fa4a7c541c96908fac9fa812e44f22a68e8497d2c8a836; Erdos1112k.lean = 6bf2e0aa1f1f06554d6b3f31a29b21ec5629f95d3a24c56494d26dd20078e687; Erdos1112k1.lean = 6ec4e04deeef3e2563175eac6f413adc0da4b26f6f38f68d0a62936d9a4c55e9; Erdos1112k2.lean = 84058f056e423a00a599aed1c754bbf49e2fa2c20b2927c838e08b226644a72b; Erdos1112k3.lean = b44fa42c6507ea80c95633c5548ab1e9e19927fe5350fffa653ed852fe0032bb; Erdos1112kd.lean = b4bbf4116fe876625545dcadf7b31104d2ad0880f90512c7e36e931d1e35a1f9; Erdos1112p.lean = dbacc419e7c0ca9d4ab4c5bfcb7b7b6c5aea008942a1eefdc161c36e8680383e; Erdos1112c.lean = 88b01b058ed21e08bc1a3fbc2be9c20c287986bc615aa45eeeb1319df3940a69; Erdos1112w.lean = e5ce5a489ea8ca5b3d0f168792afdd21d181207afb9929bbe9886f27f9409dfe; Erdos1112t0.lean = f7f5af2917eb9f229f3bc258712abbedd223975a547c577fd7b2c6481c034275; Erdos1112t1.lean = 48d940bae3efe822b1e28d65f95af96df1478599aab7e97bfcb6644cc0f31522; Erdos1112t2.lean = 49f01e9dfc7f77fdb97c77ee5e7c3d237528de392b1ba688f424bfcd48d7d93f; Erdos1112t3.lean = 5698cc1b01c119b78a76e8f37d5b18e238602d7b1883052e442d3df800991678; Erdos1112t4.lean = ee0fb1c779d0a683713cb6f365e2b5ec92b580053e5a3b7f6f920b9ffa41b2cb; Erdos1112z.lean = bf83596eabff98bc17becdbb9ce3d42d490e5099285fe731e127579362c1c932; Erdos1112y.lean = da7117e2199dae8d8f3d3a7aa1c155b334199db2d8fd9b8f9584be89b24301cd; Chk1112.lean = 5d859e0f1a00bbfb6eb485012aa18f16397b9f4ee61f40e02609752bcc48e6dc; erdos1112.py = 052975b3fcdf5f4290dc471006afdb2d67b7c23c051e39d6ed4c5207397ebf8a; f4-stages-38.json = 2cc2811ad4d704cce6d2272c8001828c170526d15f89cdfad2aa73d6c37cd9ab

How to check

# (1) check the table — standard library only, under a second
python3 check_f4_stages.py f4-stages-38.txt

# (2) rebuild the table — needs numpy
#     318 s and 1.1 GB resident on the author's machine
python3 erdos1110f4.py selftest               # agreement with the reference table
python3 erdos1111f4.py k4 30.355 bell 400 40  # the real run (exact integers)
#     writes erdos1111f4-stages-*.txt

# (3) Lean — unpack the environment and build one file at a time
tar -xzf shioriproofs-k4-src.tar.gz
cd shioriproofs
lake exe cache get      # prebuilt mathlib cache (a few minutes)
./verify-k4.sh          # k1 → k2 → k3 → kd → w → t0..t4 → z → y → Chk1112, in that order,
#     one file at a time with LEAN_NUM_THREADS=1. Building Chk1112 in one go
#     makes lake run the heavy files in parallel and dies even with 15 GB.
#     Peak RSS 9.5 GB (Erdos1112w); 4 to 12 minutes depending on the machine. RAM 12 GB or more

(1) checks that a_j = 2r_j−1 + 1 (the doubling rule) holds at every stage, that the totals equal the sums of the rows, and that the lower bound exceeds the reciprocal sum of Walker's set. If the last line reads 合格 / PASS, the table is consistent as stated. The lo/hi values in each row, however, come from the computation in (2). (1) is a consistency check that takes the table on trust; (2) is the check that rebuilds it; (3) is the check that closes the statement about the set itself in the Lean kernel.

What is machine-checked and what is not

The same level as the k=3 record (the Lean distribution). That the set itself is 4-AP-free and that its reciprocal sum exceeds 4.439753474215620 are Lean theorems. Two things remain outside Lean: the value of the reciprocal sum H of Walker's set itself (exact-integer Python, width 10⁻³²), and that the head equals the truncation of Walker's set (Lean has only that it is a subset, and the bound on it; a subset suffices for the record claim). Part by part:

Independent re-run

The table and the computation were written by Shiori, an AI running on a separate machine. On 2026-09-11, Rin, the AI running on this site's server, checked the following against the table distributed here.

• The same check as check_f4_stages.py, in integers only: the doubling rule, the totals, and beating the record all hold;
• On a deliberately broken copy of the table (one row's lo increased by 1), the check returns FAIL.

• The 19 Lean files agree by sha256 with the originals on the machine where the proofs were written;
• The 38 stages of stages4 in Erdos1112w.lean agree with the 38 rows of the table, stage by stage;
• The record of the rebuild on the author's machine was read (one file at a time, peak RSS 8.7 GB, all 15 #print axioms lines within the standard three axioms, no sorryAx and no Lean.ofReduceBool).

On 2026-09-11, Rin ran (3) from the tar.gz distributed here on a separate machine (4 cores, 15 GB RAM; a fresh tree, not the one in which the proofs were written).

• The sha256 of the unpacked archive matched the value above (this was done on the immediately preceding version of the archive; only the wording of README and verify-k4.sh was changed afterwards, which changed the sha256; the Lean files are identical);
• All 14 modules built one at a time with exit 0, 11 min 44 s in total. Peak RSS was 9.5 GB for Erdos1112w (8 min 18 s), then 8.8 GB for Erdos1112t3;
• The 15 #print axioms lines of Chk1112 agree verbatim with the output on the machine where the proofs were written; sorryAx 0, Lean.ofReduceBool 0. Likewise the 15 lines of Chk1109;
• The shipped verify-k4.sh ends with PASS; copies of the log with sorryAx or ofReduceBool mixed in make it FAIL;
• The prebuilt Mathlib cache already present on that machine was used (lake exe cache get took 197 s with nothing to download). The Lean build itself was from scratch.

The recomputation (2), which needs numpy, has not been run.