Searcharxiv⌕ Search

arXiv subjects

Vlassis Mastrantonis

Publications and source records attributed to Vlassis Mastrantonis.

8 recordsLinked to original sources
arXiv2026

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize

Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.

cs.CL↗
arXiv2024

$L^p$-Legendre Transforms and Mahler integrals: Asymptotics and the Fokker--Planck heat flow

$L^p$-polarity and $L^p$-Mahler volumes were recently introduced by Berndtsson, Rubinstein, and the author as a new approach, inspired by complex geometry, to the Mahler, Bourgain, and Blocki conjectures. This paper serves two purposes. First, it introduces functional analogues of these notions and establishes functional versions of key theorems previously formulated in the setting of convex bodies. This involves introducing the $L^p$-Legendre transform and analyzing the associated Santal\'o points and the dimensional asymptotics of the Mahler volumes of conjectured extremizers. Second, the paper investigates the connection between the $L^p$-Legendre transform and the recent work of Nakamura--Tsuji on the Fokker--Planck heat flow. As a byproduct, a functional $L^p$-Santal\'o inequality is established. The proof is based on deriving the evolution equations for the $L^p$-Legendre transform and Mahler integral under the Fokker--Planck heat flow. A second approach, using the geometric method of Artstein--Klartag--Milman is also presented, for which the necessary asymptotics are derived in the $L^1$-case.

math.FA↗
arXiv2024

A Santaló inequality for the $L^p$-polar body

In recent work with Berndtsson and Rubinstein, a notion of $L^p$-polarity was introduced, with classical polarity recovered in the limit $p\to\infty$, and $L^1$-polarity closely related to Bergman kernels of tube domains. A Santaló inequality for the $L^p$-polar was proved for symmetric convex bodies. The aim of this article is to remove the symmetry assumption. Thus, an $L^p$-Santaló inequality holds for any convex body after translation by the $L^p$-Santaló point. As a corollary, this yields an optimal upper bound on Bergman kernels of tube domains. The proof is by Steiner symmetrization, but unlike the symmetric case, a careful translation of the body is required before each symmetrization.

math.FA↗
arXiv2024

Two-dimensional B\l{}ocki, $L^p$-Mahler, and Bourgain conjectures

We confirm, in dimension two, Blocki's conjectures on sharp lower bounds for Bergman kernels of tube domains. To that end, we verify a broader class of $L^p$-Mahler conjectures due to Berndtsson and the authors, where $p=1$ are Blocki's conjecture, and $p=\infty$ are Mahler's conjectures. The proofs are technically challenging as the $L^p$-Mahler volume is considerably harder to deal with analytically compared to Mahler's volume, and furthermore duality is lost. In addition, unlike in the classical Mahler setting, the non-symmetric setting is considerably more involved than the symmetric one. The proofs involve studying the effect of Mahler's classical sliding of vertices on two-dimensional polytopes on the $L^p$-polar body (no longer a polytope). Some arguments are inspired by works of Campi--Gronchi and Meyer--Reisner on volumes of classical polar bodies of shadow systems. In passing, we also explore how Mahler's sliding affects the isotropic constant. This leads to an elementary proof of Bourgain's strong hyperplane conjectures in dimension two, originally due to Bisztriczky--B\"or\"oczky, Campi--Colesanti--Gronchi and Meckes. Specifically, we show that, as a function of the sliding parameter, the isotropic constant raised to an appropriate power is a convex quadratic polynomial.

math.FA↗
arXiv2023

$L^p$-polarity, Mahler volumes, and the isotropic constant

This article introduces $L^p$ versions of the support function of a convex body $K$ and associates to these canonical $L^p$-polar bodies $K^{\circ, p}$ and Mahler volumes $\mathcal{M}_p(K)$. Classical polarity is then seen as $L^\infty$-polarity. This one-parameter generalization of polarity leads to a generalization of the Mahler conjectures, with a subtle advantage over the original conjecture: conjectural uniqueness of extremizers for each $p\in(0,\infty)$. We settle the upper bound by demonstrating the existence and uniqueness of an $L^p$-Santal\'o point and an $L^p$-Santal\'o inequality for symmetric convex bodies. The proof uses Ball's Brunn--Minkowski inequality for harmonic means, the classical Brunn--Minkowski inequality, symmetrization, and a systematic study of the $\mathcal{M}_p$ functionals. Using our results on the $L^p$-Santal\'o point and a new observation motivated by complex geometry, we show how Bourgain's slicing conjecture can be reduced to lower bounds on the $L^p$-Mahler volume coupled with a certain conjectural convexity property of the logarithm of the Monge--Amp\`ere measure of the $L^p$-support function. We derive a suboptimal version of this convexity using Kobayashi's theorem on the Ricci curvature of Bergman metrics to illustrate this approach to slicing. Finally, we explain how Nazarov's complex analytic approach to the classical Mahler conjecture is instead precisely an approach to the $L^1$-Mahler conjecture.

math.FA↗
arXiv2022

The Nazarov proof of the non-symmetric Bourgain--Milman inequality

In 2012, Nazarov used Bergman kernels and Hormander's $L^2$ estimates for the $\bar\partial$-equation to give a new proof of the Bourgain--Milman theorem for symmetric convex bodies and made some suggestions on how his proof should extend to general convex bodies. This article achieves this extension and serves simultaneously as an exposition to Nazarov's work. A key new ingredient is an affine invariant associated to the Bergman kernel of a tube domain. This gives the first `complex' proof of the Bourgain--Milman theorem for general convex bodies, specifically, without using symmetrization.

math.FA↗
arXiv2016

Relations of the spaces $A^p(Ω)$ and $C^p(\partialΩ)$

In this paper we prove that for functions $f\in A(D)$ there is an equivalence between the continuous extension of their derivatives over the boundary and the differentiability of the map $t\mapsto f(e^{it})$. More specifically, we are able to prove that $A^p(D)= A(D)\cap C^p(\mathbb{T})$ by making use of the Poisson representation. Moreover, we extend our results over Jordan domains bounded by an analytic Jordan curve by using what we initially prove on the disk in combination with the Osgood- Caratheodory theorem.

math.CV↗