Lean 化数学会不会毁掉数学之美？圈内人激辩数学文化走向

lacker 类比数学史指出，坐标与微积分虽丑陋繁琐却更强大，最终让欧氏几何几近过时，暗指形式化证明系统 Lean 正在重演这一幕。akbirthko 延伸认为 Lean maxxing 是超智能极端功利化的产物，而数学文化对世界具有美学价值。两人激辩因此指向数学文化走向，akbirthko 预测未来可能出现一场「美学反叛」，让不可言说的价值被破坏后，学界落回某个更丰富的中间地带。