The De Bruijn–Erdős Theorem on Incidence Geometry and Near-Pencil Tightness
A complete machine-checked Lean 4 formalization of the De Bruijn–Erdős theorem (1948) in incidence geometry and pairwise balanced block designs, together with its constructive near-pencil tightness proof. Proves that any finite linear space on n ≥ 3 non-collinear points determines at least n lines (|P| ≤ |L|) via the classical combinatorial double-counting inequality. Furthermore, explicitly constructs the near-pencil configuration with designated apex p₀ (consisting of one line of n - 1 points and n - 1 lines of 2 points) and proves that it forms a valid linear space achieving exact…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-02-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000005/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'