Lean 证明推不出道德公理，形式方法救不了伦理学
AndrewSchmidtFC · x · 2026-10-12
围绕「AI 能解千禧年难题，道德哲学是否也会有 Lean 式证明」的辩论，Bradley Carson 反驳：Lean 证明只能从给定公理按固定推理规则推出结论，从不证明公理本身——而道德哲学的争议恰恰全在公理上。形式方法可以展示哪些道德前提不能共存，却无法告诉你该放弃哪一个。
「漫话AGI」频道最新
- Benjamin Bratton 发布 Agentworld 研究计划,探索人机混合社会 — bratton · 2026-10-12
- 让 AI 给改进要点、改动自己写：保住个人声音的协作法 — ctjlewis · 2026-10-12
- signulll：只需 1% 的人能造软件，供给洪流就会把软件价格打至零 — signulll · 2026-10-12
- 开发者驳「AI 有意识」论：模型只是统计计算器，意识纯属用户投射 — AlexTensor · 2026-10-12
- 超 38% 数学论文承认用了 AI,"赛博格"研究模式正在主导数学界 — emollick · 2026-10-12
- Manus 8 个月做到 1 亿美元 ARR：产品力胜过注意力打法 — parker_lyman · 2026-10-12