AI迈向数学证明的一大步，陶哲轩借AI破解数学猜想-韭研公社

登录注册

AI迈向数学证明的一大步，陶哲轩借AI破解数学猜想

逻辑KING

热爱评论的公社达人

2023-12-06 15:25:04

用AI工具辅助研究数学的项目，再一次被陶哲轩跑通！

三周前，他曾发布一篇博文，记录下自己使用Blueprint在Lean4中形式化多项式Freiman-Ruzsa猜想的证明过程。

陶哲轩表示，在整个团队中，自己贡献的代码大概只有5%。这个结果很鼓舞人心，因为这意味着数学家即使不具备Lean编程技能，也能领导Lean的形式化项目。

他发现，项目中在数学上最有趣的部分，形式化起来比较容易，而技术上看起来最显而易见的步骤，却最耗时。

而使用Blueprint将项目分解成难度小到中等的部分，效果很好，这就让大量并行工作成为可能。

这样，许多贡献者就可以处理特定的子任务，而无需理解整个证明过程，甚至可以完全不了解相关的数学领域知识。

作者利益披露：转载，不作为证券推荐或投资建议，旨在提供更多信息，作者不保证其内容准确性。

声明：文章观点来自网友，仅为作者个人研究意见，不代表韭研公社观点及立场，站内所有文章均不构成投资建议，请投资者注意风险，独立审慎决策。

信雅达

掌趣科技

昆仑万维

万兴科技

工分

1.86

投诉

复制链接

分享到微信

有用 2

打赏作者

无用

真知无价，用钱说话

0个人打赏

同时转发

暂无数据