GromovMilman
Formalization of Theorem 1 (the Gromov–Milman conjecture on polynomials restricted to subspaces) from Dol'nikov–Karasev, "Dvoretzky type theorems for multivariate polynomials and sections of convex bodies" (arXiv:1009.0392): for any even d > 0 and any k, there exists n(d, k) such that every homogeneous polynomial of degree d on R^n (n >= n(d, k)) restricts on some k-dimensional subspace V to a scalar multiple of (x_1^2 + ... + x_n^2)^(d/2). The formalization provides an unconditional, constructive proof without sorry or external topological black boxes: Carlsson's theorem on non-abelian…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-18-000025
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000025/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-18-000025/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'