随着人工智能技术的发展,数学机械化在计算机与数学交叉领域的影响越来越显著。机器证明是数学机械化领域的重要研究方向之一,指借助计算机和辅助证明程序实现定理的证明。Coq是现在国际上主流的辅助证明程序,它基于归纳构造演算的基本理论,具备严谨性与可靠性的特点。同时,Coq交互式的证明环境增强了代码的可读性。目前,Coq已被广泛应用于各类数学问题的机器证明,尤其是Gonthier和Werner在2005年利用Coq实现了著名的“四色定理”的计算机证明,增强了 Coq在学术界的影响。不等式是数学领域的重要研究课题,几乎所有数学分支学科都离不开不等式。对不等式机器证明的研究,具有普遍的应用价值。近年来不断有新成果涌现,基于数学软件Mathmatica、Maple研发的通用程序已能够机器证明某些不等式,借助辅助证明程序Coq、Isabelle、HOLLight等也实现了对一些不等式的机器证明。本文借助辅助证明程序Coq,给出了算术几何调和平均不等式、Cauchy不等式、排序不等式、Chebyshev不等式、Bernouli不等式、三角不等式和Jensen不等式这七类常用基本不等式的机器证明方法。应该指出,这些不等式及其等价命题的传统数学证明方法散见于众多文献。本文的创新点在于利用交互式定理辅助证明程序Coq,给出这些命题的形式化机器证明方法。证明过程既体现了借助Coq实现机器证明的可靠性与交互性。