原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正在试图测量一块海绵的表面积，但这块海绵是由无数不可见的微孔构成的。科学家们使用一种名为BET（以三位科学家的名字命名）的方法来估算这一面积，其原理是观察气体如何附着在海绵上。这是化学领域的一种标准工具，但有点像是在试图拼凑一幅盒盖图案模糊的拼图。
问题在于：为了得出答案，科学家们必须从实验数据中选取特定范围的数据点，并穿过这些点画出一条直线。问题在于，不同的人（或不同的计算机程序）可能会选取略有不同的范围。一个人可能会说：“让我们使用中间的 10 个点，”而另一个人则说：“不，使用中间的 12 个点。”这导致对同一块海绵得出不同的答案，从而引发困惑，并削弱了对结果的信任。
为了解决这个问题，一个团队开发了一款名为BETSI的计算机程序，它能够自动检查所有可能的数据范围，以找到“最佳”范围。这就像拥有一个机器人，它会尝试拼图块的所有可能组合，以找到完美契合的那一种。然而，即使是机器人也可能存在漏洞，或包含某些隐藏的假设，使其以微妙的方式出错。
登场：“LeanBET"——经过数学证明的机器人
本文的作者们使用一种名为Lean 4的特殊计算机工具，构建了这款机器人的新版本。请将 Lean 4 不仅仅视为一种编程语言，而是一位极其严格的数学老师，它绝不允许你在没有证明的情况下犯错。
以下是他们是如何做到的，通过一些简单的类比：
1. “双脑”系统（多态性）
通常，当你编写计算机程序时，你会使用“浮点数”（就像计算器上的数字）。这些数字运算速度快，但略有瑕疵，因为计算机无法保持无限的精度。而在进行数学证明时，你使用的是“实数”（完美、无限精度），但这些无法在计算机上直接运行。
作者们通过构建一个变形机器人解决了这一问题。
- 大脑 A（证明）： 当他们需要证明数学正确性时，机器人穿上“实数”套装。它进行完美、理论化的数学运算，以证明逻辑无懈可击。
- 大脑 B（执行）： 当他们需要在真实数据上运行程序时，机器人切换为“浮点数”套装。它在实际计算机上快速运行。
- 神奇之处： 由于机器人在两套套装中的构建方式完全相同，如果“证明大脑”确认逻辑完美，那么“执行大脑”就保证遵循相同的规则。这就像用完美的数学证明桥梁设计是安全的，然后用真实的钢材建造实际的桥梁，确信该设计能够经受住考验。
2. “食谱与烹饪”（推导即规范）
在常规科学中，你在纸上写下食谱（数学理论），然后由一位厨师（程序员）在厨房（软件）中尝试烹饪。有时，厨师会在这里或那里多加一撮盐，或者误解某一步骤，导致菜肴的味道与食谱不符。
在LeanBET中，食谱和烹饪发生在同一个房间里。“数学推导”（食谱）被直接写入代码中。计算机检查代码就是食谱本身。如果代码说“加盐”，数学证明就会验证“加盐”正是理论所要求的。理论与实践中不存在任何鸿沟。
3. “严格检查员”（形式化验证）
该论文声称，他们的程序不仅仅是猜测答案，而是随身携带一份正确性证书。
- 标准软件： 你运行程序，它给出一个数字，你希望它是正确的。
- LeanBET： 你运行程序，它给出一个数字，同时还递给你一份经过数学证明的文件，上面写着：“我检查了每一步，遵循了每一条规则，这个数字是基于你提供的数据得出的唯一正确答案。”
他们发现了什么？
他们使用 19 组不同的数据（就像 19 块不同的海绵）测试了他们新的“数学证明机器人”与旧的“标准机器人”（BETSI）。
- 结果： 在 19 块海绵中，有 18 块的两个机器人给出的答案完全一致，精确到最小的小数位。
- 唯一的小故障： 对于一块海绵（称为 UiO-66），存在微小的差异（0.03%）。作者承认他们目前尚不确定原因，但相对于实验中通常存在的噪声而言，这是一个非常小的误差。
核心结论
这篇论文并非关于发明一种测量海绵的新方法，而是关于构建现有方法的可信版本。他们将一种标准的科学工具在“数学证明”环境中重新构建，并证明其效果与旧工具一样好，同时保证没有犯任何逻辑错误。
这就像从普通地图升级到 GPS，它不仅告诉你路线，而且逐步证明该路线是可能最短且最安全的，没有任何隐藏的绕行。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。