怎样得0分？ BabyRudin习题1.1 证明有理数与无理数的和/积是无理数

诚子丶:
不要在乎别人的眼光，要知道费马主业也是律师，副业才是搞数学，到时候整个恶漩大定理让那些科班的难受几百年

【回复】费马那个年代就没啥科班这一说，都没什么人研究数学
【回复】我才不搞“空白太小写不下”这种装X遗言[嫌弃]
凛酷Rebellion:
proof 2用域公理的前提是「所有有理数的加法和乘法构成域」，而要证明这个结论还是得用proof 1的办法（当然这里只用到了封闭性和可逆性） 还有Field读错了[傲娇]

【回复】Field 读错了的确，我自己都无语了，和 file 混了。感谢提出！！[打call] 个人观点，1和2的证法都可行，但2更符合这本书的逻辑。 至于你说的“「所有有理数的加法和乘法构成域」，而要证明这个结论还是得用proof 1的办法”，我要说的是： “有理数集是域”在这本书的逻辑就是直接当真命题，无需证明，详见1.13 评注。对于这个“Rudin都不严谨”的情况，我个人观点是，任何一本数学书都有它的讨论范围，不然写起来没完没了。在一些更详细的实分析教材中，会把自然数的定义也写进去，看似很完整，但再往前推，集合论公理写了吗？即使写了集合论公理，还有数理逻辑，这样下去不是没完没了了吗？所以，总有个范围，总得有个尽头。Baby Rudin 的尽头就是默认“有理数集是域”，Rudin本人写的很清楚。
【回复】回复 @BadVortex恶漩 :我的意思是，两种证明并无太大区别。虽然proof 2可以把逻辑封装到“域”这个盒子里，但是一打开盒子就会发现，其实还是回到了有理数的定义上。
【回复】回复 @BadVortex恶漩 :哇，好厉害
Sasakiii-:
非常同意，严谨的证明就该这样。但在学校考试不可能这样写，否则根本写不完。[微笑]

【回复】老师敢这么考，这得抓多少个研究生来改卷[doge]
彼得洛夫娜奥利奥:
还是觉得中国人写的数学教材，比较容易懂 外国人写的总是跟你讲故事[doge]

【回复】回复 @-回忆_时光- :不好读，体系性也不够强，当做参考书还行，但拿来做教材确实不太合适
【回复】回复 @Fusion___ :买了上册，感觉写的太泛了
MathAgape:
刚刚回看发现自己好几个英语语法错误，我就不更正了，送给小朋友们，留作习题[doge] 还有，这个视频虽然只讲了习题1.1，但结尾把1.2-1.5的解题思路都讲过了，小朋友们可以先自己做一下，过几天来对答案[打call]

筑桥者Hagi:
这种写法适合学习形式证明软件，比如 Lean.

【回复】[星星眼][星星眼][星星眼]
Dr__Z:
如果你在大学读实分析，写成 Proof 1 那样，满分 5 分估计能拿 4 分。r != 0 的条件没考虑肯定会扣分，但 field axioms 基本上没人在乎。

【回复】这里再多说两句，如果真的去抠 field axioms，其实写成 proof 2 那样也未必严谨。因为有理数和实数本质上是两个域，c/d - a/b 那部分是在有理数域上的逆加（减法）和逆乘（除法），而 r + x 是实数域上的加法。如果想完全证明，你还要证明实数是有理数的域扩展。由于域扩展是无穷维的，这个地方要是真的展开讲的话会非常麻烦。
【回复】回复 @BadVortex恶漩 :最近我在思考一个问题，何谓数集？从自然数的基础上，人类需要减法于是有了负数。人类需要除法，于是有了有理数。人类需要解方程，于是有了代数数、复数。人类需要写程序，于是有了可计算数。然而，实数到底是怎么回事？只是为了取极限吗？但人类对于无穷操作的了解其实并不深，于是有了 axiom of choice 下的各种悖论，比如 Banach Tarski。
【回复】回复 @Dr__Z : 我也想过这样的问题，这太诡异了，如果有谁在这方面给出较好的说法，请推荐给我。
账号已注销:
请问up主是戴美瞳了吗，我老觉得你的眼睛看起来是绿的，不知道是不是错觉[脱单doge]

【回复】回复 @BadVortex恶漩 : [doge]
那不是紫苑:
这么厉害还长这么好看，，，，[打call]

Scarletmiao:
很棒，我自己肯定做不到这么严谨，不知道怎么支持e老师，就先来个3连吧

西瓜两块五一斤23:
虽然听不懂但不影响我睡不着觉想听[给心心]

窗纸346:
小姐姐比网上大多数女生能力强，鉴定完毕。

wbswlgydj:
up挺有毅力，我特么数学专业毕业的，上班后基本都忘了，平时也懒得看了，到家就想睡觉了

cjwddtc:
这个域为什么和我以前听到的群那么像呢，难道是翻译的问题吗？

家中古词:
如果是比较激进的原教旨主义者，有没有考虑过接触一下形式化证明？那样写出来的证明完全是一个程序，不会有任何直觉滑坡问题

【回复】哦～好像也有观众推荐 Lean 了，我推荐的软件是 Coq，配套书籍是 Software Foundations，作者是 Benjamin C. Pierce。 形式化证明的基本思路是在逻辑范畴里面的命题抽象为类型范畴的类型，这样命题之间的推理就可以用类型之间的转换，也就是程序表示。