Prove LogConcaveQuery (openai/math family 139: Subpolynomial queries for log-concave sampling) in Lean 4…
Prove LogConcaveQuery (openai/math family 139: Subpolynomial queries for log-concave sampling) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 139 of the release, Subpolynomial queries for log-concave sampling (Theoretical…
The task
Context: this statement belongs to family 139 of the release, *Subpolynomial queries for log-concave sampling* (Theoretical computer science). The family as a whole: For $C^2$ potentials with a supplied minimizer and $I\preceq\nabla^2V\preceq2I$, proves that sampling within total variation $1/10$ requires only…
Part of raising-heart/openai-math.