Searcharxiv⌕ Search

arXiv subjects

Weikun He

Publications and source records attributed to Weikun He.

18 recordsLinked to original sources
arXiv2026

Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility. In this paper, we propose the paradigm that directly uses a general coding agent as a formal math reasoner. This paradigm is motivated by (1) A general coding agent provides a natural interface for diverse reasoning tasks beyond proving, (2) Performance can be improved by simply replacing the underlying base model, without training, and (3) MCP enables flexible extension and autonomous calling of specialized tools, avoiding complex design. Based on this paradigm, we introduce Numina-Lean-Agent, which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean, retrieval of relevant theorems, informal proving and auxiliary reasoning tools. Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all problems in Putnam 2025 (12 / 12), matching the best closed-source system. Beyond benchmark evaluation, we further demonstrate its generality by interacting with mathematicians to successfully formalize the Brascamp-Lieb theorem. We release Numina-Lean-Agent and all solutions at https://github.com/project-numina/numina-lean-agent.

cs.AI↗
arXiv2025

Effective equidistribution of random walks on simple homogeneous spaces

We consider a random walk on a homogeneous space $G/\Lambda$ where $G$ is a non-compact simple Lie group and $\Lambda$ is a lattice. The walk is driven by a probability measure $\mu$ on $G$ whose support generates a Zariski-dense subgroup. We show that the random walk equidistributes towards the Haar measure unless it is trapped in a finite $\mu$-invariant set. Moreover, under arithmetic assumptions on the pair $(\Lambda, \mu)$, we show the convergence occurs at an exponential rate, tempered by the obstructions that the starting point may be high in a cusp or close to a finite orbit. The main challenge is to show that the dimensional properties of a given probability distribution on $G/\Lambda$ improve under convolution by $\mu$. For this, we develop a new method, which combines a dimensional interpolation result and a dimensional increase alternative. This approach allows us to bypass inherent geometric obstructions. To show dimensional interpolation, we establish a general subcritical projection theorem under optimal non-concentration assumptions on the projector, and a corresponding submodular inequality for irreducible representations which allows its application to random walks. Both are of independent interest. The dimensional increase alternative aligns with the spirit of Bourgain's projection theorem. It is fine-tuned for random walks and has the advantage of being valid in situations lacking transversality.

math.DS↗
arXiv2025

Khintchine dichotomy and Schmidt estimates for self-similar measures on $\mathbb{R}^d$

We extend the classical theorems of Khintchine and Schmidt in metric Diophantine approximation to the context of self-similar measures on $\mathbb{R}^d$. For this, we establish effective equidistribution of associated random walks on $\text{SL}_{d+1}(\mathbb{R})/\text{SL}_{d+1}(\mathbb{Z})$. This generalizes our previous work which requires $d=1$ and restricts Schmidt-type counting estimates to approximation functions which decay fast enough. Novel techniques include a bootstrap scheme for the associated random walks despite algebraic obstructions, and a refined treatment of Dani's correspondence. Along the way, we also establish non-concentration properties of self-similar measures near algebraic subvarieties of $\mathbb{R}^d$.

math.DS↗
arXiv2024

Khintchine dichotomy for self-similar measures

We establish the analogue of Khintchine's theorem for all self-similar probability measures on the real line. When specified to the case of the Hausdorff measure on the middle-thirds Cantor set, the result is already new and provides an answer to an old question of Mahler. The proof consists in showing effective equidistribution in law of expanding upper-triangular random walks on $\text{SL}_{2}(\mathbb{R})/\text{SL}_{2}(\mathbb{Z})$, a result of independent interest.

math.DS↗
arXiv2024

Multislicing and effective equidistribution for random walks on some homogeneous spaces

We consider a random walk on a homogeneous space $G/\Lambda$ where $G$ is $\mathrm{SO}(2,1)$ or $\mathrm{SO}(3,1)$ and $\Lambda$ is a lattice. The walk is driven by a probability measure $\mu$ on $G$ whose support generates a Zariski-dense subgroup. We show that for every starting point $x \in G/\Lambda$ which is not trapped in a finite $\mu$-invariant set, the $n$-step distribution $\mu^{*n}*\delta_{x}$ of the walk equidistributes toward the Haar measure. Moreover, under arithmetic assumptions on the pair $(\Lambda, \mu)$, we show the convergence occurs at an exponential rate, tempered by the obstructions that $x$ may be high in a cusp or close to a finite orbit. Our approach is substantially different from that of Benoist-Quint, whose equidistribution statements only hold in Ces\`aro average and are not quantitative, that of Bourgain-Furman-Lindenstrauss-Mozes concerning the torus case, and that of Lindenstrauss-Mohammadi-Wang and Yang about the analogous problem for unipotent flows. A key new feature of our proof is the use of a new phenomenon which we call multislicing. The latter is a generalization of the discretized projection theorems \`a la Bourgain and we believe it presents independent interest.

math.DS↗
arXiv2023

On the dimension theory of random walks and group actions by circle diffeomorphisms

We establish new results on the dimensional properties of measures and invariant sets associated to random walks and group actions by circle diffeomorphisms. This leads to several dynamical applications. Among the applications, we show, strengthening of a recent result of Deroin-Kleptsyn-Navas [24], that the minimal set of a finitely generated group of real-analytic circle diffeomorphisms, if exceptional, must have Hausdorff dimension less than one. Moreover, if the minimal set contains a fixed point of multiplicity k + 1 of an diffeomorphism of the group, then its Hausdorff dimension must be greater than k/(k + 1). These results generalize classical results about Fuchsian group actions on the circle to non-linear settings. This work is built on three novel components, each of which holds its own interest: a structure theorem for smooth random walks on the circle, several dimensional properties of smooth random walks on the circle and a dynamical generalization of the critical exponent of Fuchsian groups.

math.DS↗
arXiv2022

The Final Model Building for the Supersymmetric Pati-Salam Models from Intersecting D6-Branes

All the possible three-family ${\cal N}=1$ supersymmetric Pati-Salam models constructed with intersecting D6-branes from Type IIA orientifolds on $T^6/(\mathbb{Z}_2\times \mathbb{Z}_2)$ are recently presented in arXiv: 2112.09632. Taking models with largest wrapping number $5$ and approximate gauge coupling unification at GUT scale as examples, we show string scale gauge coupling unification can be realized through two-loop renormalization group equation running by introducing seven pairs of vector-like particles from ${\cal N}=2$ sector. The number of these introduced vector-like particles are fully determined by the brane intersection numbers while there are two D6-brane parallel to each other along one two-torus. We expect this will solve the gauge coupling unification problem in the generic intersecting brane worlds by introducing vector-like particles that naturally included in the ${\cal N}=2$ sector.

hep-th↗
arXiv2022

Semisimple random walks on the torus

We study linear random walks on the torus and show a quantitative equidistribution statement, under the assumption that the Zariski closure of the acting group is semisimple.

math.DS↗
arXiv2022

The Complete Search for the Supersymmetric Pati-Salam Models from Intersecting D6-Branes

We construct a systematic method to build all the possible three-family ${\cal N}=1$ supersymmetric Pati-Salam models from Type IIA orientifolds on $\mathbb{T}^6/(\mathbb{Z}_2\times \mathbb{Z}_2)$ with intersecting D6-branes, in which the $SU(4)_C\times SU(2)_L \times SU(2)_R $ gauge symmetry can be broken down to the $SU(3)_C \times SU(2)_L \times U(1)_Y$ Standard Model gauge symmetry by the D-brane splitting and supersymmetry preserving Higgs mechanism. This is essentially achieved by solving all the common solutions for the RR tadpole cancellation conditions, ${\cal N}=1$ supersymmetry conditions, and three generation conditions with deterministic algorithm. We find that there are $202752$ possible supersymmetric Pati-Salam models in total, and show that there are only $33$ independent models with different gauge coupling relations at string scale after modding out equivalent relations, such as T-dualities, etc. In particular, there is one and only one independent model which has gauge coupling unification. Furthermore, one can construct other types of intersecting D-brane models utilizing such deterministic algorithm, and therefore we suggest a brand new method for D-brane model building.

hep-th↗
arXiv2021

Trou spectral dans les groupes simples

Nous montrons la propriété du trou spectral pour la famille des graphes de Cayley obtenus par réduction modulo $q$ d'un sous-groupe de $\mathrm{SL}_d(\mathbb{Z})$ dont l'adhérence de Zariski est un $\mathbb{Q}$-groupe simple. -- We show a spectral gap property for the family of Cayley graphs obtained by reduction modulo $q$ of a subgroup of $\mathrm{SL}_d(\mathbb{Z})$ whose Zariski closure is a simple $\mathbb{Q}$-group.

math.GR↗
arXiv2021

Equidistribution of affine random walks on some nilmanifolds

We study quantitative equidistribution in law of affine random walks on nilmanifolds, motivated by a result of Bourgain, Furman, Mozes and the third named author on the torus. Under certain assumptions, we show that a failure to having fast equidistribution is due to a failure on a factor nilmanifold. Combined with equidistribution results on the torus, this leads to an equidistribution statement on some nilmanifolds such as Heisenberg nilmanifolds. In an appendix we strengthen results of de Saxce and the first named author regarding random walks on the torus by eliminating an assumption on Zariski connectedness of the acting group.

math.DS↗
arXiv2021

Sum-product for real Lie groups

We prove a discretized sum-product theorem for representations of Lie groups whose Jordan-Hölder decomposition does not contain the trivial representation. This expansion result is used to derive a product theorem in perfect Lie groups.

math.GR↗
arXiv2020

Linear random walks on the torus

We prove a quantitative equidistribution result for linear random walks on the torus, similar to a theorem of Bourgain, Furman, Lindenstrauss and Mozes, but without any proximality assumption.

math.DS↗
arXiv2020

Affine random walks on the torus

We consider random walks on the torus arising from the action of the group of affine transformations. We give a quantitative equidistribution result for this random walk under the assumption that the Zariski closure of the group generated by the linear part acts strongly irreducibly on $\mathbb{R}^d$ and is either Zariski connected or contains a proximal element. Specifically, we give quantitative estimates (depending only on the linear part of the random walk) for how fast the random walk equidistributes unless the initial point and the translation part of the affine transformations can be perturbed so that the random walk is trapped in a finite orbit of small cardinality. In particular, we prove that the random walk equidistributes in law to the Haar measure if and only if the random walk is not trapped in a finite orbit.

math.DS↗
arXiv2019

Random walks on linear groups satisfying a Schubert condition

We study random walks on $\mathrm{GL}_d(\mathbb{R})$ whose proximal dimension $r$ is larger than $1$ and whose limit set in the Grassmannian $\mathrm{Gr}_{r,d}(\mathbb{R})$ is not contained any Schubert variety. These random walks, without being proximal, behave in many ways like proximal ones. Among other results, we establish a Hölder-type regularity for the stationary measure on the Grassmannian associated to these random walks. Using this and a generalization of Bourgain's discretized projection theorem, we prove that the proximality assumption in the Bourgain-Furman-Lindenstrauss-Mozes theorem can be relaxed to this Schubert condition.

math.DS↗
arXiv2018

Orthogonal projections of discretized sets

We generalize Bourgain's discretized projection theorem to higher rank situations. Like Bourgain's theorem, our result yields an estimate for the Hausdorff dimension of the exceptional sets in projection theorems formulated in terms of Hausdorff dimensions. This estimate complements earlier results of Mattila and Falconer.

math.CA↗