Searcharxiv⌕ Search

arXiv subjects

Wensheng Yu

Publications and source records attributed to Wensheng Yu.

13 recordsLinked to original sources
arXiv2026

Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations

Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language models (LLMs) and interactive theorem provers, intelligent agents offer a promising approach to automating the formalization of mathematical theories. This paper presents the Math Foundation Formalization Agent (MFF-Agent), a general-purpose intelligent agent designed to support formalization tasks across multiple mathematical domains. The agent integrates the reasoning capabilities of large language models with the formal verification capabilities of the Rocq proof assistant. It incorporates task classification, tool-assisted execution, verification feedback, and state-based task management to support the generation, refinement, and verification of formal proofs. Unlike an approach focused on a single mathematical theory, the agent is examined through case studies involving Morse--Kelley axiomatic set theory (MK), real numbers, propositional logic, and equivalences of the axiom of choice. These cases investigate its applicability across mathematical foundations and distinguish source-level completion, interactive verification, and reproducible compilation. The results demonstrate the feasibility of a unified operational framework for heterogeneous foundation-level tasks and clarify the gap between such a framework and a fully integrated mathematical foundation.

cs.LO↗
arXiv2026

Optimal Configurations for Mordell's Problem

Mordell's problem asks for the largest product of squared pairwise distances among $n$ points in the complex plane with a prescribed sum of squared distances from the origin. When this sum equals $n$, the maximum for $2\le n\le5$ is known to be $n^n$, attained precisely by the $n$th roots of unity up to rotation and relabeling. For $n\ge6$, Chalk showed that a regular polygon together with its center gives a larger product than the regular $n$-gon. We prove that for $6\le n\le9$ the maximum is $(n-1)^{n-1}r_n^{n(n-1)}$, where $r_n=\sqrt{n/(n-1)}$. Up to the same symmetries, the unique maximizer consists of the origin and the vertices of a regular $(n-1)$-gon of radius $r_n$. For six points, algebraic elimination reduces the proof to an exact comparison of stationary values. For seven points, we compare all twelve classes in a published classification of equilibria. For eight and nine points, rigorous interval arithmetic establishes an inequality for every admissible pair. Summing over pairs gives the sharp global bound, and the equality conditions determine the configuration. An explicit ten-point comparison and a known instability result together exclude Chalk's configuration for every $n\ge10$. For each $n$ from two through eight, Mordell's problem and the minimum-diameter problem studied by Bateman and Erdős have a common optimal configuration.

math.CO↗
arXiv2026

On the Five-Point Case of Mordell's Problem

For five complex points $z_1,\ldots,z_5$ satisfying $\sum_i|z_i|^2=5$, Mordell's discriminant inequality states that $\prod_{i<j}|z_i-z_j|^2\leq5^5$, with equality precisely for a unit regular pentagon, up to rotation and permutation. We organize its proof around a direct comparison of discriminant values. A global maximizer gives a centered stationary configuration, whose coefficient equations reduce the generic case to two quartic branches. On each branch, the absolute value of a cubic polynomial gives the original discriminant objective after accounting for the normalization scale. Exact rational interval bounds exclude both branches from the maximum, and the exceptional coefficient cases leave the regular pentagon. The argument determines the maximizing configuration without reconstructing all stationary shapes. We have completed a full Lean formalization of the five-point inequality and both directions of its equality condition, including all reductions and finite checks used in this proof.

math.CV↗
arXiv2026

A Finite Certificate for the Positive $n=11$ Vasc Inequality

We establish the Vasc cyclic inequality for all strictly positive real eleven-tuples by a finite exact certificate. Cyclic rotation places a minimum at the first position, and rank words together with cumulative gaps reduce the problem to $10!=3{,}628{,}800$ homogeneous integer polynomials of degree eleven. Independent coefficient reconstruction proves $3{,}358{,}617$ roots directly. The remaining $270{,}183$ roots are covered by $267{,}952$ ordinary midpoint certificates, $2{,}195$ complete binary subdivision certificates, and $36$ complete certificates containing partial sorting nodes. Each nontrivial leaf is checked by subtracting weighted AM-GM midpoint circuits from a positive multiple of the transformed polynomial and verifying every residual coefficient. Explicit word-set comparisons certify disjointness and exact coverage. We prove the soundness of the leaves and both subdivision rules, then recover the rational inequality by positive denominator clearing and continuity. The resulting proof combines explicit mathematical reductions with independently checked exact integer certificates.

cs.SC↗
arXiv2024

Formalization of the Filter Extension Principle (FEP) in Coq

The Filter Extension Principle (FEP) asserts that every filter can be extended to an ultrafilter, which plays a crucial role in the quest for non-principal ultrafilters. Non-principal ultrafilters find widespread applications in logic, set theory, topology, model theory, and especially non-standard extensions of algebraic structures. Since non-principal ultrafilters are challenging to construct directly, the Filter Extension Principle, stemming from the Axiom of Choice, holds significant value in obtaining them. This paper presents the formal verification of the Filter Extension Principle, implemented using the Coq proof assistant and grounded in axiomatic set theory. It offers formal descriptions for the concepts related to filter base, filter, ultrafilter and more. All relevant theorems, propositions, and the Filter Extension Principle itself are rigorously and formally verified. This work sets the stage for the formalization of non-standard analysis and a specific real number theory.

math.LO↗
arXiv2019

Formalization of the Axiom of Choice and its Equivalent Theorems

In this paper, we describe the formalization of the axiom of choice and several of its famous equivalent theorems in Morse-Kelley set theory. These theorems include Tukey's lemma, the Hausdorff maximal principle, the maximal principle, Zermelo's postulate, Zorn's lemma and the well-ordering theorem. We prove the above theorems by the axiom of choice in turn, and finally prove the axiom of choice by Zermelo's postulate and the well-ordering theorem, thus completing the cyclic proof of equivalence between them. The proofs are checked formally using the Coq proof assistant in which Morse-Kelley set theory is formalized. The whole process of formal proof demonstrates that the Coq-based machine proving of mathematics theorem is highly reliable and rigorous. The formal work of this paper is enough for most applications, especially in set theory, topology and algebra.

cs.LO↗
arXiv2006

Easily Testable Necessary and Sufficient Algebraic Criteria for Delay-independent Stability of a Class of Neutral Differential Systems

This paper analyzes the eigenvalue distribution of neutral differential systems and the corresponding difference systems, and establishes the relationship between the eigenvalue distribution and delay-independent stability of neutral differential systems. By using the ``Complete Discrimination System for Polynomials", easily testable necessary and sufficient algebraic criteria for delay-independent stability of a class of neutral differential systems are established. The algebraic criteria generalize and unify the relevant results in the literature. Moreover, the maximal delay bound guaranteeing stability can be determined if the systems are not delay-independent stable. Some numerical examples are provided to illustrate the effectiveness of our results.

math.DS↗
arXiv2006

Solution to the Generalized Champagne Problem on Simultaneous Stabilization of Linear Systems

The well-known "Generalized Champagne Problem" on simultaneous stabilization of linear systems is solved by using complex analysis \cite{A73,C78,G69,N52,R87} and Blondel's technique \cite{B94,BG93,BGMR94}. We give a complete answer to the open problem proposed by Patel et al. \cite{P99,PDV02}, which automatically includes the solution to the original "Champagne Problem" \cite{BG93,BGMR94,BSVW99,LKZ99,P99,PDV02}. Based on the recent development in automated inequality-type theorem proving \cite{Y98,Y99,YHX01,YX05,YX03}, a new stabilizing controller design method is established. Our numerical examples significantly improve the relevant results in the literature \cite{LKZ99,PDV02}.

math.DS↗
arXiv2002

Stability of Polytopic Polynomial Matrices

This paper gives a necessary and sufficient condition for robust D-stability of Polytopic Polynomial Matrices. Edge theorem is extended to multi-input-multi-output case.

math.OC↗
arXiv2002

Geometric Characterization of Strictly Positive Real Regions and its Applications

Strict positive realness (SPR) is an important concept in absolute stability theory, adaptive control, system identification, etc. This paper characterizes the strictly positive real regions in coefficient space and presents a robust design method for SPR transfer functions. We first introduce the concepts of SPR regions and weak SPR regions and show that the SPR region associated with a fixed polynomial is unbounded, whereas the weak SPR region is bounded. We then prove that the intersection of several weak SPR regions associated with different polynomials can not be a single point. Furthermore, we show how to construct a point in the SPR region from a point in the weak SPR region. Based on these theoretical development, we propose an algorithm for robust design of SPR transfer functions. This algorithm works well for both low order and high order polynomial families. Illustrative examples are provided to show the effectiveness of this algorithm.

math.OC↗
arXiv2002

Robust SPR Synthesis for Low-Order Polynomial Segments and Interval Polynomials

We prove that, for low-order (n < 5) stable polynomial segments or interval polynomials, there always exists a fixed polynomial such that their ratio is SPR-invariant, thereby providing a rigorous proof of Anderson's claim on SPR synthesis for the fourth-order stable interval polynomials. Moreover, the relationship between SPR synthesis for low-order polynomial segments and SPR synthesis for low-order interval polynomials is also discussed.

math.OC↗
arXiv2002

On the Number of Positive Solutions to a Class of Integral Equations

By using the complete discrimination system for polynomials, we study the number of positive solutions in {\small $C[0,1]$} to the integral equation {\small $ϕ(x)=\int_0^1k(x,y)ϕ^n(y)dy$}, where {\small $k(x,y)=ϕ_1(x)ϕ_1(y)+ϕ_2(x)ϕ_2(y), ϕ_i(x)>0, ϕ_i(y)>0, 0<x,y<1, i=1,2,$} are continuous functions on {\small $[0,1]$}, {\small $n$} is a positive integer. We prove the following results: when {\small $n= 1$}, either there does not exist, or there exist infinitely many positive solutions in {\small $C[0,1]$}; when {\small $n\geq 2$}, there exist at least {\small 1}, at most {\small $n+1$} positive solutions in {\small $C[0,1]$}. Necessary and sufficient conditions are derived for the cases: 1) {\small $n= 1$}, there exist positive solutions; 2) {\small $n\geq 2$}, there exist exactly {\small $m(m\in \{1,2,...,n+1\})$} positive solutions. Our results generalize the existing results in the literature, and their usefulness is shown by examples presented in this paper.

math-ph↗