Pseudorandom hypergraph matchings (Ehard–Glock–Joos)
A Lean 4 / Mathlib formalization of the main results of Ehard, Glock and Joos, "Pseudorandom hypergraph matchings" (Combin. Probab. Comput. 2020): Pippenger's theorem on almost perfect matchings in almost regular hypergraphs with small codegrees (Theorem 1.1); the existence of a matching M in any r-uniform hypergraph with Δ(H) ≤ Δ, codegrees ≤ Δ^{1−δ} and at most exp(Δ^{ε²}) edges such that ω(M) = (1 ± Δ^{−ε}) ω(E(H))/Δ simultaneously for up to exp(Δ^{ε²}) weight functions (Theorem 1.2, with ε = δ/(50r²)); the generalization to weight functions on ℓ-tuples of edges, under the same…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-17-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-17-000004/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-10-17-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'