元宇宙里掀起回憶殺？這波虛擬懷舊營銷主打一個極限反差
來源：首席品牌官從被稱為“元宇宙元年”的2021年開始，幾乎所有品牌都在迫不及待地“入駐”元宇宙。而一提及品牌們的元宇宙玩法，相信多數人腦海里首先浮現
快來圍觀，陶哲軒當視頻博主了。
第一個產出就很炸裂：人類需要寫滿一頁紙的證明，結果借助 AI 33 分鐘就搞定了？！
整個過程看起來一氣呵成，還是全程“盲證”不用過腦子那種。
對于這一操作，網友們驚呆：這具有足夠的歷史意義。
在沒有明顯引導、宣傳之下，他的訂閱數一天時間已經有 900+，觀看數超兩千，目前仍然在高速增長中。
大家趕在爆火之前留言：
今天我們相聚在這里，就是為了見證偉大數學頻道的誕生。
具體來看看是如何做到？
33 分鐘盲證定理陶哲軒這次選取了泛代數中的一個命題，即證明 Magma 方程 E1689 蘊含 E2。
方程具體是什么不重要，我們只需要了解，即使是方程理論項目的合作者 Bruno Le Floch，也足足人工花了一頁紙才完成證明。
而用上 AI 后，整個證明過程僅用時 33 分鐘：
具體而言，陶哲軒嘗試完全基于 Bruno Le Floch 的草稿，逐行進行形式化。
他將草稿拆分為微小邏輯單元，交由 GitHub 生成代碼骨架，再以 Lean 的 canonical 策略匹配填補細節，過程中也涉及部分手動補全。
最終，整個形式化證明能夠在 Lean 中通過驗證。
不僅時間大大縮短了，更重要的是滿足了“人類可讀性”。
要知道 Bruno Le Floch 最初挑戰該問題時，曾在論文中宣稱 E1689-E2 的所有已知證明都依賴計算機輔助。
直到后來他使用 prover9 ATP（自動定理證明器）給出了一個更具可讀性的人類版本，所以才對之前的想法產生動搖：
它是否仍然可以被認為是計算機輔助的，我不確定。
針對這一疑惑，陶哲軒提議今后可以在論文中明確說明，雖然最初的證明是由計算機生成的，但在項目進行過程中，研究者們成功地將其轉化為一個人類可讀的證明。
并且為了實際驗證 AI 能在多大程度上開啟自動化形式證明，陶哲軒就此開啟了本次 YouTube 首秀。
通過幾次親自嘗試，陶哲軒得出了如下結論：
這種半自動化的方法適用于那些技術性強、概念性弱的論證，即那些主要關注細節準確性而非整體概念理解的證明。
并且他再一次強調，AI 輔助證明能夠把數學家從一些相對不重要的繁瑣事務中解放出來，“讓 AI 去做一些它擅長的事”。
在他看來，盡管最終的結果“并不優雅”，但它體現了 AI 輔助證明的巨大潛力。
最后需要說明一下，陶哲軒并非一次就成功了。
據他在視頻中透露，前兩次的證明過程都出現了一些“bug”——
第一次拿到的代碼才到第 5 行他就有點看不懂了，所以選擇了重開；第二次雖然完成了所有證明（用時 48 分鐘），但由于是新人博主不太熟悉錄屏設備，導致屏幕分享失敗，因此又只能重來。
數學證明助手迎來 2.0 版本此外，還有他開發的數學證明助手迎來 2.0 版本升級。
根據介紹，這是一個用 Python 開發的輕量級證明助手，其功能遠遜于 Lean、Isabelle 或 Rocq 等完整證明助手，但（希望）它能夠輕松用于證明一些簡短而繁瑣的任務。
一個具體的目標是，為漸近分析提供支持。
兩周前，在大模型的幫助之下，他花了四個小時編程得到了這么一個概念驗證工具。
結果不到兩周，這個工具就迎來了全面改進 ——
首先，將其改造成一個基本的證明助手，使其能夠處理一些命題邏輯；其次，根據反饋，這個證明助手變得更為靈活（在幾個關鍵方面刻意模仿精簡證明助手）。
目前這個助手有兩種模式：假設模式和策略模式。其中策略模式作為默認模式，有點類似于 Lean、Isabelle 或 Rocq 里面那樣式兒的策略模式。
目前策略列表主要分為四類：
命題策略（主要圍繞通過布爾運算操縱命題）
線性算術策略（依賴于線性規劃及其變體）
替代策略 —— 用一個假設或目標替代另一個假設或目標的各種技術
簡化策略 —— 利用其他可用假設來“簡化”假設或目標的方法
當然這些還不是全部，這個助手支持擴展，大家可以在里面進行添加。
舉個例子。
如果 x，y，z 是正實數，且 x<2y 和 y<3z+1，證明 x<7z+2。
將它形式化就會變成：
>>>frommainimport*>>>p=linarith_exercise()Startingproof.Currentproofstate:x:pos_realy:pos_realz:pos_realh1:x<2*yh2:y<3z+1|-x<7*z+2證明助手接收到指令后，指導助手使用各種“策略”來簡化問題，直到問題得到解決。
那么這個問題可以通過線性算術 Linarith () 求解。
>p.use(Linarith())Goalsolvedbylineararithmetic!Proofcomplete如果想要有詳細解釋，也是 OK 的：
>>>frommainimport*>>>p=linarith_exercise()Startingproof.Currentproofstate:x:pos_realy:pos_realz:pos_realh1:x<2*yh2:y<3*z+1|-x<7*z+2>>>p.use(Linarith(verbose=true))Checkingfeasibilityofthefollowinginequalities:1*z>01*x+-7*z>=21*y+-3*z<11*y>01*x>01*x+-2*y<0Infeasiblebysummingthefollowing:1*z>0multipliedby1/41*x+-7*z>=2multipliedby1/41*y+-3*z<1multipliedby-1/21*x+-2*y<0multipliedby-1/4Goalsolvedbylineararithmetic!Proofcomplete!可以看到，首先，它通過反證法進行論證，即采用否定 x≥7z+2 目標 x<7z+2 并將其添加到假設中。
然后，它將假設中所有不等式轉化為“線性規劃”形式，變量在左邊，常數在右邊。
最后，它使用精確線性規劃來尋找這些不等式的線性組合，從而導致荒謬的不等式，在這種情況下 0<1。
解決完問題之后，還可以使用 proof（）進行檢查。
有時候，遇到證明過程會涉及案例拆分的情況，那么證明助手最終會呈現樹狀結構。
對于這個證明助手，陶哲軒表示：非常滿意，并且愿意接受進一步的建議或貢獻新的功能。比如引入新的數據類型、公例和策略，或者貢獻一些有難度的例子。
此外還計劃開發用于估算符號函數的函數空間規范的工具。例如創建部署霍爾德不等式和索博列夫嵌入不等式等定理的策略。看起來 sympy 框架足夠靈活，可以為這類對象創建更多的對象類。
感興趣的朋友，可以前往去體驗下哦。
參考鏈接：
[1]https://mathstodon.xyz/@tao/114486537464033675
[2]https://www.youtube.com/watch?v=cyyR7j2ChCI
[3]https://github.com/teorth/estimate_tools/blob/master/EstimateTools/test/equational.lean
本文來自微信公眾號：量子位（ID：QbitAI），作者：白交一水
本文鏈接：http://www.www897cc.com/showinfo-45-12809-0.html陶哲軒油管首秀：33 分鐘，AI 速證「人類需要寫滿一頁紙」的證明
聲明：本網頁內容旨在傳播知識，若有侵權等問題請及時與本網聯系，我們將在第一時間刪除處理。郵件：2376512515@qq.com
Copyright ? 2016-2023 天津谷騏科技有限公司 版權所有 sitemap.xml
違法及侵權請聯系：2376512515@qq.com 津ICP備18001702號
津公網安備 12010102000574號