专栏名称: 清熙
清晰、客观、理性探讨大模型(LLM)、人工智能(AI)、大数据(Big Data)、物联网(IoT)、云计算(Cloud)、供应链数字化等热点科技的原理、架构、实现与应用。
今天看啥  ›  专栏  ›  清熙

数学领域最大的突破之一 LEAN 如何将数学引入编码,将编码引入数学

清熙  · 公众号  ·  · 2024-09-15 17:36

文章预览

编译:王庆法 译者注:LEAN作为函数式编程语言,用途包括形式数学、软硬件验证、用于数学和代码合成的AI,以及数学和计算机教育。国内关于LEAN的介绍文章少的可怜,这么强大的工具,与数学、计算机软硬件、代码和AI都如此繁荣的国内形式严重不匹配。本文改编自 Leo de Moura 在 2024 年 7 月的计算机辅助验证国际会议 (CAV) 上发表的主题演讲。 译者注:OpenAI o1 不会只是个 Text-to-Lean引擎吧  2 013 年,我启动了  Lean 项目 ,目标是弥合自动的和交互式定理证明器之间的差距。自成立以来, Lean 在数学界得到了无与伦比的应用 ,超过了以前在形式化数学方面的其他努力。 最新版本 Lean 4  是用 Lean 本身实现的,也是一种成熟的可扩展编程语言,具有 强大的 IDE 支持 、 包管理和蓬勃发展的生态系统 。 2023 年,Sebasian Ullrich 和我创立了 Lean焦点 研究 ………………………………

原文地址:访问原文地址
快照地址: 访问文章快照
总结与预览地址:访问总结与预览