{"id":"palomar/PALOMAR-2026-10-18-000025","url":"https://github.com/akopjan/Dolnikov-Karasev-Gromov-Milman/tree/a32fae66a704d736f0c2c3ec9b14afd22979fe9f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000025-v1.json","repo":"https://github.com/akopjan/Dolnikov-Karasev-Gromov-Milman","tags":["math.MG","math.DG","math.AT","math.CO","msc:52A20","msc:55M20","msc:55M35","msc:14P99","convex-geometry","polynomials"],"score":0,"title":"GromovMilman","trust":"high","domain":"math.MG","source":"palomar","authors":["Arseniy Akopyan"],"reviews":0,"subject":"math.MG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"Dvoretzky type theorems for multivariate polynomials and sections of convex bodies","identifier":"arXiv:1009.0392 [math.MG]","relationship":"formalizes"}]}