论码农与数学家的相似性【数学地图】【重构数学2/4】

零号稻草人:
说的太好了。在今天，形式化数学已经众多营销号口中的糟粕。但是形式化数学依旧在方法论的领域里引导着数学的研究与发展，尤其随着AI的发展，形式化数学又焕发了新的生机。

【回复】回复 @YARTSA :“随时”可能有点低估形式化的难度和工作量了。就好比程序员说我不用高级语言用汇编也能写出一样的程序一样，可行，但难度和工作量也是客观的。
【回复】这…营销号不懂数学吧…虽然我们写证明用的是自然语言，但是我们可以随时翻译成形式语言…（利益相关：纯数研究生在读）
【回复】有点儿剧透了啊[脱单doge]
醉姒123:
在现代社会中，数学和编程都是非常重要的技能。人们都认为，如果你懂得数学，你就可以理解科学和技术的基础，而如果你会编程，你就可以利用计算机来完成各种任务。但是，为什么在应试教育下，学生往往擅长数学，却不会编程呢？应试教育下的目的是要让学生在短时间内记忆大量的知识，以便应对考试。在这种环境下，时间是非常宝贵的，所以老师会让学生利用宝贵的时间进行题海战术刷题。而数学作为一门基础学科，在应试教育中更是占据了重要的地位。数学本来可以帮助多数学生锻炼逻辑思维、分析问题能力和计算能力，但是在应试教育下，数学沦为了强记考试，一经考完，就会忘记。编程是一个完全不同的领域。与数学不同，编程更强调实践和体验，需要学生去亲自动手实践、编写程序。编程是一门需要创造力、主动性和思维交互性的学科，需要学生在解决问题时发挥自己的创造性思维和动手能力。而这些能力并不是仅仅通过纸上考试就可以轻松掌握的。在应试教育模式中，老师是学生头上“唯一正确”的存在，他/她讲什么就是什么，学生只需要记忆和模仿。而在现代（编程）教育中，老师的角色更多的是指导者和辅导者，学生需要自主探索和实践，寻找解决问题的方法。编程教育强调的是培养学生的实践能力、动手能力和团队协作能力，而这些能力在传统应试教育中比较难得到锻炼。数字与符号是一种更加抽象的概念，而编程则更加地物化和实际。在数学中，学生往往需要进行抽象思考，也就是需要把看到的东西用数字或符号表示出来，这样才能从中找到规律和解决问题。而在编程中，人们需要将想象力转化为代码，这样计算机才能在程序中正确执行所需的任务。这两种方式虽然都有需要处理逻辑的因素，但是因为它们与世界的交互方式不同，所以需要不同的思考方式和技巧。数学和编程是两个完全不同的技能领域，每一个领域所要求的思考方式、技巧、实践方法和学习兴趣也大相径庭。对于数学好编程不好的学生来说，他们可能更加擅长处理抽象的符号和数字，但相对不强调实际操作和自主解决问题的编程学习环境下就会显得吃力了。

【回复】最为可悲的是数学和编程方面的人才如果不应试，都不一定能考上好学校,而且编程竞赛普遍对考试没帮助,数学竞赛就业相对困难
【回复】回复 @曲名真楠 :没，大部分学校都没有，省实验郑州外国语有可能会有，有社团的高中在河南回来连百分之1都没有。
醉姒123:
数学好不一定编程就好，这两者逻辑就不同

【回复】数学好的，愿意学编程可就能好，数学很强调逻辑思维能力。
河马大叔又回来啦:
初中时候，经常想问题想到头痛。觉得很多书本上的知识都是在循环论证。觉得定义没有清楚，后面的计算完全没有意义。非常痛苦。

【回复】就因为这个我大学才报了数学专业，本人有点强迫症，不严谨的东西很难接受。大学本科四年最享受的是学拓扑学和图论，非常享受那种从基本定义严密推理出各种定理的过程。后来迫于生存压力，硕士转了计算机，现在已经是牛马码农一枚了。
【回复】没办法，中学到大学本科阶段的数学知识有限且结构粗糙。仅仅能讲个表面就差不多了。严格的讲即使是运算层面也不够完备。[笑哭]
【回复】代码就是学别人写好的函数库，硬件软件都是，90百分之的，都不用重复造轮子
因特斯特拉:
数学跟代码没有半毛钱关系，码农可以不懂数学，数学家也可以不懂代码。

【回复】如果你数学好的话，你会发现“存在不懂数学的码农”与“存在不懂代码的数学家”为真，不能推导出“数学跟代码不存在任意关系”为真。
【回复】你是既不懂数学，也不懂写代码[吃瓜]
【回复】回复 @TongYonjim : 所以你编程的时候自己推一遍吗？程序员需要的是快速使用，而不是证明，懂吗。金字塔尖的东西你还去重复造轮子？
醉姒123:
编程是对脑力要求极高的工种，说的通俗点就是要求脑袋瓜子很灵活，喜欢动脑的人，学起来更顺畅些。说的高大上一点就是逻辑思维能力强，很多人对位到数学好，其实也不全对。逻辑思维主要是要求对一些事物具备归纳，梳理能力。和数学不完全一码事，当然数学好一些的，逻辑思维更加流畅这倒是事实。编程是一个不断的完善自己知识体系的过程，完善梳理自己的知识体系就需要自己脑袋不停的运转。在这说到一点，很多学习编程就喜欢用视频去学习，看的不亦乐乎。然后离开视频让写程序然后眼前一抹黑。喜欢中国的应试教育模式去学习编程，在编程界这个模式不怎么好用，要学编程自学能力一定要强，技术知识多更新又这么快，没有持续的自学能力去跟进也是容易被淘汰。说这么多不是说，学编程就不能用视频去学习，学的时候不能完全依赖视频要有自己独立思考的时间。起码也有让自己大脑去思考，构架自己知识体系的时间。

【回复】编程对脑力没啥要求其实感觉，只要你不去搞算法造轮子或者是自己开始架构一个项目，只要不涉及这仨，我感觉编程就是个体力活，你敲就完了，你能想到的功能都有人帮你写好了轮子，你只需要查然后用。
【回复】目前主流的编程语言都不难，你想，当程序员这个职业都可以被教育机构批量制造出来时，说明了这个职业不难，更深一点看其实就是这个职业是有一定的标准化和体系化程度的，标准化和体系化在程序员这个职业中基本上指的就是编程框架，工具，库，用这些东西在编写代码的时候其自身就给出了一个包装好的方法和规范约定，那么讨论这个事情从实际行业需求来说绝对是合理的，在实际开发中只需要会使用框架和遵守团队规范就能搭建出优秀的程序，根本不需要过多逻辑思维能力。加上现在工具越来越发达，大量易用框架和AI工具，学习成本是很低的，也没你说的跟不上，除非摆烂了。所以你说的编程这个工种，其实大部分人的工作都是很简单的，只有少部分的人在开发框架和库。当然大部人在系统的学习下都不可能直接是框架，所以会觉得难，实际工作中你学的也用不到多少，会发现别人早就给你一堆工具，方法了，全都给你包了，程序员越到后面也是这样子，为了效率开发谁还自己写，用别人的就行了
【回复】回复 @amazy2023 :没调过屎山代码吧，写代码也许是体力活，但读代码、调代码是纯纯的脑力活。
DL909:
很悲哀的是，没有bug的数学体系已经被证明是不可能的。

【回复】没学明白导致的 集合论，模型论，证明论读了吗？ 一致性、完备性、可判定性分别是什么系统的什么性质？ 哥德尔不完备定理的适用条件是什么？
【回复】看看围棋象棋的纯人棋谱演变过程就了然了（棋谱必然存在漏洞）。人的认识是受限的。生也有涯，学也无涯；以有涯随无涯，殆矣。[笑哭]
【回复】谁告诉你哥德尔ban的是一致性？
三藩市天晴洛杉矶明朗:
我感觉把一些都公理化形式化是一个很朴素的想法，为什么到计算机出现这个进程才被加快呢

【回复】1921年希尔伯特数学大会都有雏形了，计算理论1930年迸发，计算机1940年才有，构造演算1980完成。最近重新火不代表上世纪不存在。
【回复】就像Curry-Howard对应，它的朴素想法叫做BHK解释。编程语言是一种精确媒介，它迫使人们扫除心中的模糊之处。
【回复】这个可以看一下我的上一期视频～
若宫千希:
我自己的经验是，作为程序员去了解一些证明论和类型论的知识，甚至不用十分深入，都能够获得不少对于类型以及“利用类型来确保程序正确性”的insight。LEAN也是个对于即使是非此领域的人来说都十分友好的工具。 So! For fun and profit! 来学一学吧！ (btw, theorem proving 相关还有另一条从模型论出发的路子，代表性的工作是z3，同样很有趣)

【回复】(再感叹一句，我接触过的veri相关的工具 lean, z3, tla+ 都是 msr 出来的，巨硬的好东西真不少
【回复】回复 @HELI_SPIRIT :函数的本质？我日常嫌弃为什么要发明态射却把函数钉死在小范畴里而不是直接把命题函数和函数关系的定义分别严格化，以及日常埋汰交换图。 另外 Joachim Lambek 知道吧，楼里好像没人提，我把他的活补进去跟着 C-H correspondence 一起黑了。 文小刚不熟，看起来还是南部阳一郎搞的东西更有意思。[doge]
【回复】所以建议大家没事的时候都学学Typescript和Scala, 做一下类型体操
平衡天客の云:
感觉程序可以添加一个点亮的功能，把自己学过的数学内容从整个网络中可视化出来，以此规划自己的学习路径√ 应该……不会很难实现吧[doge][doge]

【回复】有没有可能，你再说一种东西：思维导图
【回复】也可以倒过来，点某个点标出前置知识
【回复】回复 @KiritanTakechi : 高度怀疑我们任何一方有看懂对方在说什么
厌夜shooter:
我似乎猜到下一期要说的内容了，通过现有知识形式化后，利用gpt寻找其深层次规律，然后泛化到未知领域，可以在现有基础上推广更多的定理，也可以穿透新的命题至底层，例如连续统假设依赖于公理选择一样。 这在未来会有多伟大的力量，完全不可知，突然感到后脊发麻。

【回复】回复 @慕青QAQ : 我说的是公理选择，不是选择公理... 我想表达的是AI也许可以很快得出连续统假设这种在常规公理体系下不可判定，而需要增加额外公理的命题。
【回复】个人感觉，推理出连续统假设依赖于选择公理还或许过于困难了
【回复】咋这么多人才发现。。。这其实就是入门级的AGI。[脱单doge]
寿司屋的营业:
从四维讲到机器辅助证明，都是我最喜欢的……太赞了

AI视频小助理:
一、数学向公理化发展的历史和形式化数学的概念，并通过计算正弦函数的近似值来认识基本的程序语言概念。 00:01 - 介绍数学向公理化发展的历史和公理化数学的定义 00:40 - 数学家们设计形式化证明的方法，利用计算机代码一样的形式语言来写出无懈可击的严谨证明 01:52 - 探讨数学及代码的概念，介绍了Python编程语言的基本概念和如何计算正弦函数的近似值 二、函数的实现和使用，以及程序员在工作中常用的术语。通过阶乘函数和计算通项公式的代码例子，展示了函数在编程中的重要性。 03:24 - 函数的实现是将输入数据转化为输出结果的流水线 03:59 - 函数的输入和输出类型决定了它可以实现的功能 05:36 - 程序员常用的术语包括调包、造轮子和祖传代码 三、代码和数学之间的相似性，探讨了大型程序中过时问题的处理难度，以及如何用代码证明定理。 06:41 - 操作系统等大型程序的代码是由多位程序员共同创作的，时间推移会导致过时和问题代码积累。 07:14 - 写代码和证明定理有相似之处，可以类比为函数的输入和输出。 09:31 - 用代码表示定理的证明，可以实现从前提到结论的流水线。 四、如何使用计算机来证明数学定理，以及数学和代码之间的关系。同时，还介绍了形式化证明语言的种类和使用方法。 10:00 - 通过函数实现计算过程，得到证明。 10:34 - 变量类型代表命题为真的证据，但不包含证明细节。 11:44 - 数学家和计算机科学家设计了多种形式化证明语言，如MATHLAB和MASLIP。 五、MATLAB中关于实数的定义和性质，以及Mathlip中代码的引用关系图。形式化的发展对于数学知识的重构和发展具有重要作用。 13:26 - MATLAB用有理数的科系列的方式 来构造性的定义的实数 14:27 - MATLAB的代码是公开的，每个人都可以画出自己的数学地图 16:08 - 形式化带给我们的影响 可能远比严谨这个锦上添花的愿望要深远得多 --本内容由AI视频小助理生成，关注解锁AI助理，由@熠熠攸攸 召唤发送

xa_0002:
上个礼拜我还查到有人介绍Curry-Howard同构了。不得不说之前听过一个道理，当你听说一个新的概念，你会发现过了一小会身边就会瞬间出现一堆这种概念XD。不过这里跟这个道理大概没什么关系，大概只是自己在上个视频基础上搜了一堆东西正好搜到了（）

【回复】过分采集用户信息的大数据推荐算法导致的[吃瓜]
【回复】荣格的共时性现象，也是在说类似的问题，很奇妙哈哈。
HELI_SPIRIT:
很多人被形式化这几个字吓住了，因为不会使用symbol，symbol只是用来绑定概念的。根本不存在什么形式化。

【回复】可以从最基本的解释器写起
木几工丂:
完了，我的学生时代数学成绩不好，看来在码农这条路上的上限已经被封死了[笑哭]

【回复】你哪怕从初中数学到高中数学，补一下，最多不到一周，在补高等数学个个方向也很快啊，主要是你平时的用，用得上才行
【回复】回复 @木几工丂 :计算机图形学：你好
【回复】回复 @幻の上帝 :难道说几何和解析几何也没用？[笑哭]
月下梧桐s:
可以让计算机使用这些形式化的公理、定理自行推导新的结论么？最终应该会生成很多人类从未想过或者想过但未证明的命题

【回复】可以的，但是体系里总会有无法证明也无法证伪的命题，参见哥德尔不完备定理。
【回复】希尔伯特当初也是这样想的
【回复】外行人认为这程序肯定很艰编
菠萝resuming:
我有一个很喜欢数学的朋友，如果能嫖到up的程序，发给他，他肯定受用hhhhh期待