一位数学家描述了如何使用AI模型结合Lean、文学编程和LaTeX实时撰写并验证数学证明。
AI translation, not an official translation. Refer to the original for technical details.
Adapted from @nasqret我在数学领域测试了 GPT-Astra，这是一次量子级的飞跃。你可以与模型对话，并在Lean中实时证明命题。那种感觉令人叹为观止。你可以验证自己的想法，编译出真理。对于一位数学家来说，这种感觉就像我们终于进入了一个可以将全部精力投入构思与探索的时代。一旦逻辑确立，每条引理便水到渠成。以前验证工作总是滞后，但Astra非常快速，对于许多任务来说，当你在Codex中写下论证时，形式化工作便同步完成了。 如果你让模型使用文学编程加LaTeX，最终得到的将是你的证明与Lean代码的融合——一切都按照你书写时的方式加以阐释，其中穿插着小段易于消化的Lean代码。 我不想再回到那个证明的唯一确认方式只是"啊哈"的时代了。现在，"啊哈"之后紧随着一个绿色对勾，它真真切切地告诉你，你已经抓住了本质。试想一下，如果世界上所有的引理都汇聚在一个庞大的数据库中，并指向发现它们的人和模型，那将是多么美妙。你可以组合并融汇自己的想法，站在巨人的肩膀上继续前行。而如今，你看得更远，建得更快。我们才刚刚处于这些变革的起点。还有那么多工作要做，还有那么多乐趣等待着我们！
