【重构数学4/4】未来的重构：数学、代码与人工智能

[@zhw7635]

我自己用lean做cs方向一段时间了，然后试了一下用mathlib学一些本科数学，印象比较深的点有两个：（1）反馈相比光看书强太多了，做证明题和例题马上知道自己对不对，（2）和写代码一样，有时我并不care某个东西的具体实现，只是想拿来用，等到需要再去了解；自己看书很难达到这样的效果，因为对于一个我不理解的定理，我不能保证我一定能用对，但是用lean的话我能知道我是否漏了某些条件。个人觉得这种便利性可以提高效率。

[@yugu233]

有趣的经验。请问你是用lean学习全新的课程呢，还是已经有一些基础的课程，学习巩固呢？

[@c2co2co32-]

輔助證明可以，取代不可能，純粹上的不可能，因為在"已定的邏輯系統"下不存在自我建構又自我說服能力的邏輯系統(一般認為可以放進去是因為你做的題目框架寫好了，不會問自證邏輯系統的問題，相當於你滿足了哥德爾完備性定理，所以題目都能成功跑出來)
更直觀來說，目前AI還無法滿足某些邏輯學問題，如圖靈測試，情況一，當跑出一個所有人都不懂的證明，他就過不了圖靈測試，因為證明看不懂就等於亂碼
情況二，證明能看懂，那又會發生另一個問題，證明的語意是哪來的，倘諾只是依照邏輯系統本身的產出，那就不等於獨立證明，相當於依照設定好的邏輯系統運行，等於不用手算上機跑，那可不叫AI
假設既能看懂、而邏輯系統也不是一開始設定好的，也就是該AI自行補充邏輯系統來完備證明，那恭喜你，你不只發明了一個AI可以證明數學，還創造了第一個AI數學家，這是相當困難的，相當於創造一個客觀上有思維的AI
更白話的講，現在的AI有能力證明數學問題，但不是"獨立"證明，得拿現有的東西訓練語言模型產生數學證明
順帶一提，不完備定理的理解魔怔了，那是無設限的情況下去找一個特殊命題，即所有邏輯系統都無法產生證明但該命題存在，正常來說，不用杞人憂天每次都覺得存在一個無法證明的命題，因為更大的可能是遇不上，不要每次都只會提不完備定理，多數情況更有用的是完備性定理，他保障你的程式碼理想情況下，跑出來的結果必定具有邏輯效力

[@無名氏-l1c]

剛看完陶哲軒演講演算法就給我推你的影片

[@John-de9vd]

长见识了，非常感谢推荐lean工具

[@jim1977]

说的很有道理，确实大模型的出现之后，数学需要进行重构，才能达到更好的和人类交流

[@FlAsChang]

1:50 lean code 是如何成功證明的？跟代碼的關聯性為何？很適合開幾期來教學一下！

[@yugu233]

ruclips.net/video/b59fpAJ8Mfs/видео.html 片段引自这个视频，可以看一看

[@hanna8399]

lean + LLM 普及之后，那数学就是工科了🤣

[@lovehwt]

重构数学！

[@louis-dieudonne5941]

更新了！🎉

[@FlAsChang]

出片了！！

[@andrewwolf2404]

你好可爱😍