陶哲軒上手Copilot：不可思議，它能從定理名字猜出我想要的方向

AIGC動(dòng)態(tài)歡迎閱讀

原標(biāo)題：陶哲軒上手Copilot：不可思議，它能從定理名字猜出我想要的方向

關(guān)鍵字：定理,不等式,重寫,論文,表達(dá)式

文章來源：機(jī)器之心

內(nèi)容字?jǐn)?shù)：2113字

內(nèi)容摘要：機(jī)器之心報(bào)道編輯: 蛋醬、小舟嘗鮮 GPT-4 之后，陶哲軒又用上了 Github Copilot。這一次，他的試用場景是學(xué)習(xí) Lean 語言并利用其形式化數(shù)學(xué)定理。對于大模型來說，形式化的定理證明也算一種挑戰(zhàn)。形式化證明本質(zhì)上是一種計(jì)算機(jī)程序，但與 C++ 或 Python 中的傳統(tǒng)程序不同，證明的正確性可以用證明助手（比如 Lean 語言）來驗(yàn)證。定理證明是代碼生成的一種特殊形式，在評估上非常…

原文鏈接：點(diǎn)此閱讀原文：陶哲軒上手Copilot：不可思議，它能從定理名字猜出我想要的方向

聯(lián)系作者

文章來源：機(jī)器之心

作者微信：almosthuman2014

作者簡介：專業(yè)的人工智能媒體和產(chǎn)業(yè)服務(wù)平臺(tái)