数学定理的计算机形式化证明，近年来随着计算机科学的迅猛发展，特别是证明辅助工具Coq的出现，取得了长足的进展。 Coq是一个交互式定理证明与程序开发系统，可用于描述定理内容和验证定理证明。Coq 的交互式编译环境使用户以人机对话的方式一问一答，边设计边修改，使证明中的疏漏及时得到补证。进入21世纪以来，随着“四色定理”、“有限单群分类定理”及“Kepler 猜想”等一系列著名数学难题形式化证明的实现，各种计算机证明辅助工具在学术界得到广泛认可。 滤子扩张原则(Filter Extension Principle)是滤子(filter)相关理论中的一个重要定理，它断言每一个滤子都可以扩张成为一个超滤(ultrafilter)。非主超滤(non-principal ultrafilter)作为一类特殊超滤，在逻辑学、集合论、拓扑学、模型论等领域均有运用。特别地，非主超滤还可用于代数结构的非标准扩张，例如非标准分析基础——超实数(hyper-real numbers)的构造。目前尚未见到直接构造非主超滤的方法，其存在性一般需要借助选择公理(Axiom of Choice)进行证明。作为选择公理的结论，滤子扩张原则可简化非主超滤存在性的证明，使其在形式化的过程中更易使用。 滤子扩张原则的形式化基于Coq中的Morse-Kelley(MK)公理化集合论形式化系统。MK公理化集合论承认比集合更广之“类(class)”作为基本研究对象，一个类被称为集合当且仅当它可属于任意另一个类。相比数学上使用较多的Zermelo-Fraenkel(ZFC)公理化集合论，MK是ZFC的真扩展，在形式化过程中使用起来更为便利。 滤子扩张原则的形式化涉及诸多滤子概念，包括且不限于滤子(filter)、超滤(ultrafilter)、主超滤(principal ultrafilter)、非主超滤(non-principal ultrafilter)等。所有相关定义、定理以及滤子扩张原则均在Coq证明工具中得到完整形式化描述和验证。