证明助手中的认证计算

Question

手动或由计算机代数系统执行的符号计算可能是错误的或仅在某些假设下成立。一个经典的例子是sqrt(x^2) == x，一般情况下，这不是真的，但如果x是实数且非负，则它确实成立。

是否有使用证明助手/检查器（例如 Coq、Isabelle、HOL、Metamath 或其他）来证明符号计算的正确性的示例？我特别对微积分和线性代数示例感兴趣，例如求解定积分或不定积分、微分方程和矩阵方程。

更新： 更具体地说，了解是否有微积分和线性代数方面的本科作业示例可以正式解决（可能在证明助理的帮助下），以便解决方案可以通过自动验证证明检查器。这里有一个非常简单的精益作业示例。

Answer 1

对于 Coq 证明助手，有几个库可以提供帮助。Coquelicot（https://gitlab.inria.fr/coquelicot/coquelicot）非常符合您的要求。Coquelicot 团队做了一个练习，并参加了法国 baccalaur\xc3\xa9at - 我想说更像是大学而不是高中数学考试 - 并完成了练习的大部分证明。证明可以在此处的示例中找到（https://gitlab.inria.fr/coquelicot/coquelicot/-/tree/master/examples）。我考虑过将练习和答案翻译成英文。

\n

但这是几年前的事了，同时针对特定应用程序有非常强大的工具。例如，有 coq-interval ( https://gitlab.inria.fr/coqinterval/interval )，它完全自动地对相当复杂的不等式进行 Coq 证明，比如一个高阶多项式与某个区间内具有某个最大值的正弦函数相匹配偏差。它通过泰勒分解并计算残差的上限来实现这一点。它还可以对各种数值积分进行错误证明。最近添加的一项新功能是能够绘制经过验证的正确绘图。

\n

Gappa 是 Coq 中证明无限精度实数和浮点计算之间误差的工具（https://gitlab.inria.fr/gappa/gappa）。

\n

另一个非常有趣的 Coq 开发是 CoRN（https://github.com/coq-community/corn），它是 Coq 中构造实数的形式化。构造实数是可以计算的真实实数。本质上，构造性实数是一种将数字计算到任何所需精度的算法，并证明该算法收敛。人们可以证明这些数字满足实数的所有常见属性。构造实数的一个有趣的副作用是它们只需要 LPO 作为公理，而在经典实数中，实数本身的存在就是一个公理。您在 CoRN 中进行的任何计算（例如 pi>3）都会自动被证明是正确的。

\n

所有这些工具都包含在 Coq Platform 中，Coq Platform 是 Coq 证明助手的常见发行版。

\n

还有更多，而且还在稳步增加。我想说，在不久的将来，我们就会拥有一个可用且经过验证正确的 CAS。

\n