arXiv Science⌕ Search

arXiv subjects

Guowei Dou

Publications and source records attributed to Guowei Dou.

4 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

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