代码之家  ›  专栏  ›  技术社区  ›  Yury

数学证明助手

  •  7
  • Yury  · 技术社区  · 10 年前

    大多数校对助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反,我对最适合数学的证明助手(例如微积分)感兴趣。你能推荐一个吗?我听说过Mizar,但我不喜欢源代码是封闭的,但如果它最适合数学,我会使用它。像Agda和Idris这样的新语言适合数学证明吗?

    1 回复  |  直到 10 年前
        1
  •  12
  •   gallais    10 年前

    Coq 拥有涵盖真实分析的广泛库。脑海中浮现出各种发展:

    • 这个 standard library 以及建立在其基础上的项目,例如现在已经失效的 coqtail 项目[1](广泛涵盖幂级数,并在复数上做了大量工作)或更近期的 coquelicot 所有这些都依赖于实数的公理化定义 presented here .

    • 更具建设性的方法是 the C-CoRN 该项目从实际构建reals开始。

    解决现实问题的另一种方法是转向非标准分析。这是人们使用的 ACL2 一直在做。

    对于该领域的更一般的视图,您可能应该阅读 this survey paper coquelicot项目的相关人员。

    [1] 完全披露:我参与了那个项目

    推荐文章