Mathematica 与 Lean 的双向可拓展交互

Minchao Wu (Wolfram|Alpha 顾问)

我们介绍一个 Mathematica 与定理证明器 Lean 的双向可拓展交互连接。该连接通过翻译两个系统中的语法使得用户能够在两个系统交换任意信息。作为应用，我们介绍如何使用 Lean 的元编程来验证 Mathematica 的计算，以及使用 Mathematica 来引导在 Lean 中的证明。另一方面，我们演示如何在 Mathematica 中浏览和搜索 Lean 的定理库。