Searcharxiv⌕ Search

arXiv subjects

Xiayimei Han

Publications and source records attributed to Xiayimei Han.

3 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↗
arXiv2020

Hodge Representations

Hodge representations were introduced by Green-Griffiths-Kerr to classify the Hodge groups of polarized Hodge structures, and the corresponding Mumford-Tate subdomains of a period domain. The purpose of this article is to provide an exposition of how, given a fixed period domain $\mathcal{D}$, to enumerate the Hodge representations corresponding to Mumford-Tate subdomains $D \subset \mathcal{D}$. After reviewing the well-known classical cases that $\mathcal{D}$ is Hermitian symmetric (weight $n=1$, and weight $n=2$ with $p_g = h^{2,0}=1$), we illustrate this in the case that $\mathcal{D}$ is the period domain parameterizing polarized Hodge structures of (effective) weight two Hodge structures with first Hodge number $p_g = h^{2,0} = 2$. We also classify the Hodge representations of Calabi-Yau type, and enumerate the horizontal representations of CY 3-fold type. (The "horizontal" representations those with the property that corresponding domain $D \subset \mathcal{D}$ satisfies the infinitesimal period relation, a.k.a. Griffiths' transversality, and is therefore Hermitian.)

math.AG↗