作者查詢 / xcycl
作者 xcycl 在 PTT [ Math ] 看板的留言(推文), 共241則
限定看板：Math
看板排序：
全部MAC325Math241AdvEduUK240iOS198Gossiping127bicycle105Coffee87PhD85PLT55AfterPhD54Programming39FITNESS34BabyMother32C_Chat28studyabroad27sex26feminine_sex22Germany21LaTeX20HatePolitics19IELTS19book18TOEFL_iBT18CSSE17homemaker17MobileComm12logic11sinica10study10C_and_CPP9Android8NTU8Python8home-sale7DigiCurrency6E-appliance6nCoV20196Oversea_Job6Soft_Job6Tech_Job6creditcard5Japandrama5NSwitch5Brit-pop4C_Sharp4clmusic4FuMouDiscuss4MacShop4PublicIssue4CompBook3marriage3NCKU_Math3China_Travel2global_univ2KS98-3022Mix_Match2Prob_Solve2rent-exp2Salary2Violin2Bank_Service1Boy-Girl1CATCH1ForeignEX1Google1Headphone1Key_Mou_Pad1LCD1Linux1London1Militarylife1movie1Tennis1VISA1<< 收起看板(74)
1F→: 這邊有點太神話 Lean ，它並不具備「理解」的能力11/09 21:21
2F→: 簡單說是數理邏輯（或型別論）的實作，能夠檢查證明11/09 21:22
3F→: 的有效性。因為語言很底層，要把現代數學完整形式化11/09 21:24
4F→: 而且要能夠以數學家可以理解的形式是還有一段路要走11/09 21:25
10F→: 這兩個翻譯是普遍性的問題，就想像教科書所有的命題11/11 13:19
11F→: 全部都只用數理邏輯的符號表達11/11 13:19
12F→: 旁邊可以用自然語言的註解，但 Lean 只看符號的部分11/11 13:20
13F→: 就跟寫程式一樣，預期的行為跟實際可能不一樣11/11 13:20
8F噓: 英文相關的文章提到 AI 頂多是輔助的角色05/11 18:16
9F→: 怎麼到了中文世界文章就變成主角了？05/11 18:16
67F→: 程式語言不是只能寫 float，是能夠寫 exact real 的06/21 00:02
55F推: Constructive proof 下寫出來的證明就是可判定程式08/10 07:54
56F→: 喔！08/10 07:54
57F→: 可判定程式指的是有限時間內可計算出結果的程式。08/10 07:56
58F推: 但在直構邏輯內又可以證明所有的實數不可數，這一08/10 08:54
59F→: 時難說明清楚，還是先去看點現代構造式數學的介紹08/10 08:54
60F→: 搞懂點基礎，不然迷糊仗打不完。08/10 08:54
69F→: https://doi.org/10.1090/bull/155608/09 02:50
70F→: 這篇把構造式數學講得很清楚08/09 02:51
71F→: 這篇是專業的數學家深入淺出講得很好08/09 02:52
72F→: 不要浪費時間看上面業餘的解釋了08/09 02:52
73F→: （我指的是上面的推文）08/09 02:53
110F→: 我不大確定你想的「一般的構造式證明」有沒有定義08/09 10:18
111F→: 構造式數學是完全可以當作數學理論來討論08/09 10:18
112F→: 不是一開始還在探索的哲學概念（或者說「主義」）08/09 10:20
113F→: 當然沒受過相關教育或訓練的人不會曉得很正常08/09 10:20
114F→: 原 po 說了想問這方面的專業知識，那這些「啟發」性08/09 10:23
115F→: 的想法不就是來亂的嗎？08/09 10:24
135F推: 原 po 都問到電腦能不能算，不是曖昧不明的 proof08/09 11:06
136F→: by construction 了。08/09 11:06
146F→: 「一開始的問題」是指什麼？08/09 12:35
147F→: 如果是古典數學的實數，那用 negative translation08/09 12:36
149F→: 翻譯到構造式數學上討論08/09 12:37
153F→: 我不想重複論文上面說的，那篇寫得也沒有很難08/09 12:44
169F→: 啊，抱歉，我原本說的「上面的推文」並不是針對08/09 13:34
170F→: hwanger 而是整體推文看下來的，想說為什麼這麼激烈08/09 13:35
171F→: 才想到我是接在 hwanger 下回的，有這層意思08/09 13:36
1F→: 大概是根據 greatest element 推出是 successor 吧01/30 16:33
27F→: 反正知道能夠詮釋到基礎，實際都是在抽象語言操作11/22 21:32
28F→: 細究用什麼系統跟詮釋與在上面做數學關係不大11/22 21:33
29F→: 除非是做邏輯相關的問題，這些在數學影響不大11/22 21:35
30F→: 總之後設語言的討論是確保數學推論可以進行11/22 21:36
31F→: 而不是反過來讓自己綁手綁腳陷在這些細節裡頭11/22 21:37
15F→: 把 3 編成集合是一種，也可以自然定義一進位系統11/22 16:13
16F→: 這樣 3 只是這個系統下 S(S(S0)) 的代稱11/22 16:14
17F→: 用純符號系統不直接透過集合論比較方便檢驗11/22 16:15
18F→: 當然這些符號定義的方式要符合某種形式規範11/22 16:15
19F→: 這些形式規範設計的時候可以統一討論語意11/22 16:16
20F→: 最後當然還是可以編碼到集合論上，但不需要跑到底層11/22 16:16
23F→: 反過來找數學基礎的領域稱為 reverse mathematics11/22 13:42
24F→: 也不是什麼賺大錢沒事幹的人做的吧11/22 13:43
25F→: 化約的話不見得要翻成更低階的系統11/22 13:43