6 papers
Formalization of Filter-Method Construction for Real Numbers in Coq
Guowei Dou, Wensheng Yu
This paper presents a formalization for a theory of constructing real numbers using concepts related to filters. The formalization is implemented using the Coq proof assistant and…
Math Foundation Formalization Agent: A General-Purpose Approach to Formalizing Mathematical Foundations
Jiaxin Xie, Guowei Dou, Xiang Ji +1
Mathematical formalization plays an important role in establishing rigorous and machine-verifiable foundations for mathematical reasoning. With the development of large language mo…
An Alternative Proof of the SPR Synthesis Theorem for Polynomial Segments of Arbitrary Order
Zhengtai Xiong, Tiancheng Xu, Xiang Ji +3
For any positive integer n and any two monic real Hurwitz polynomials of degree n, every convex combination of the two is Hurwitz stable if and only if there exists a common numera…
On the Five-Point Case of Mordell's Problem
Tiancheng Xu, Guowei Dou, Wensheng Yu
For five complex points satisfying , Mordell's discriminant inequality states that , with equality precisely for a…
Robust Strictly Positive Real Synthesis for Sixth-Order Interval Polynomial Families
Tiancheng Xu, Guowei Dou, Xiang Ji +2
Every Hurwitz-stable interval family of monic real polynomials of degree six admits a single real numerator of degree six that makes all the associated transfer functions strictly…
Formalization of the Filter Extension Principle (FEP) in Coq
Guowei Dou, Wensheng Yu
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-princi…