Canonization and the Overhang
6 days ago
- #software-engineering
- #mathematics
- #LLMs
- 大卫·贝西斯认为，数学过于重视定理证明，而低估了创造力、清晰度和教学的重要性，这些因素对于进步至关重要。
- LLM驱动的定理证明器可以在不依赖人类协作和直觉有益副作用的情况下证明定理。
- 在软件领域，通过测试的代码与为团队可用性和迭代而进行社会建构的代码之间存在着类似性。
- 规范化是将一次性解决方案转化为可重用、连贯且兼容的系统或库的过程，这一过程耗时但具有长期价值。
- 软件通过规范化的代码受益于稳定的抽象和可靠的系统，这与可丢弃、单次使用的软件形成对比，后者在传统标准下可能显得'糟糕'。
- '知识悬置'指的是来自过去创造力的未实现潜力，连接现有想法可以产生新的解决方案，这一概念既适用于数学也适用于软件。
- LLM适合通过记忆和跨大规模文本库的模式匹配来搜索'知识悬置'，而人类则依赖于直觉飞跃。
- 开源软件代表了可基于其进行未来开发的规范化工作的'知识悬置'。
- 仅重视定理证明或编码而不进行规范化和知识传播，可能会耗尽'知识悬置'并低估清理和教学等关键的'衔接工作'。