Tingzhou Wei | Searcharxiv

arXiv2026

Sharp Bounds on the Independence Number of Simplicial Spheres

We study the maximum size of an independent set in the graph of a simplicial sphere. Let $\beta(d,n)$ denote this maximum over all simplicial $(d-1)$-spheres on $n$ vertices, and let $\alpha(d,n)$ denote the maximum restricted to flag $(d-1)$-spheres. For every fixed $d\geq4$, we prove $\beta(d,n)=n-\Theta(n^{1/\lfloor d/2\rfloor})$. For flag spheres, we show $\alpha(d,n)\geq n-4\sqrt n+O(1)$ for all $d\geq4$ and determine the correct asymptotic order $\alpha(d,n)=n-\Theta(\sqrt n)$ for dimensions $d=4,5$. We also investigate the independence sets of Bier spheres and show that, in contrast to our other results, for this very large family of spheres, the independence number cannot be larger than $\left\lfloor\frac{n}{2}\right\rfloor.$

math.CO↗

arXiv2026

Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory

Asymptotic statistical theory is a challenging domain for AI-assisted formalization: its central results mix convergence statements, asymptotic expansions, functional analysis, and regularity conditions that have a large gap from existing infrastructure in Lean 4 formalization. To address these challenges, we propose a hypothesis-disciplined Lean 4 formalization pipeline built from multiple agents: a manager that coordinates seven specialist roles for proof planning, skeleton scaffolding, Mathlib reconnaissance, proof construction, integration, independent review, and audit. The main methodological discipline is the hypothesis-disciplined audit, implemented by the Auditor agent: every main-theorem hypothesis and concept-layer field must be anchored in the source mathematical prose, justified as a Lean encoding adapter, marked as source-implied, or rejected as an unsupported strengthening. Using this workflow, we build a systematic formalization of asymptotic statistical theory, especially the parametric and semi-parametric models' asymptotic distribution and efficiency results. The resulting Lean development is axiom-clean and source-faithful, with Lean-checked and human-audited proofs of core parametric and semi-parametric theorems organized so that theorem-agnostic infrastructure and statistical concept definitions are separated from theorem-specific assembly. The formalization results are available at https://github.com/junwei-lu/Lean-Asymptotic-Statistical-Theory.

cs.AI↗