Counterexamples in type systems (2021)22 days agohttps://counterexamples.org/该文本列举了类型系统中的31个反例，涵盖了多态引用、协变容器、变体检查和递归等问题。涉及的主题包括对象构造、Curry悖论、运行时类型信息错误、重载以及子类型与继承。其他要点涉及自私性、隐私侵犯、不稳定表达式、规避问题、作用域逃逸和全称量化。本整理由Stephen Dolan完成，感谢Andrej Bauer、Leo White和Jeremy Yallop的贡献，并包含视觉主题切换功能。
Human mathematicians are being outcounterexampleda day agohttps://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outc...ChatGPT 推翻了埃尔德什单位距离猜想；数学家们证实了这一点，但最初没有在 Lean 中形式化。Logical Intelligence 在 Lean 中自动形式化了反例，鲍里斯·阿列克谢夫利用 OpenAI 的 Sol 模型实现了完整的 Lean 形式化，三周内生成了 120 万行 Lean 代码。在一次研讨会上，一篇关于有限平坦群概形的 AI 生成论述包含了一个错误主张；AI 识别并为此提供了反例。AI 通过 Sol 和 Fable 发现了格罗滕迪克关于阶为 n 的群概形问题的反例。阿基尔·马修在 Lean 中将其形式化，并加入了 mathlib。Sol 和 Fable 等 AI 工具加速了数学项目的形式化进程，例如模性提升定理，并正成为研究人员不可或缺的助手。Fable 发现了长期未解的雅可比猜想的一个反例。保罗·勒泽奥将其形式化，DeepMind 的存储库促进了验证过程。AI 生成的数学需要形式化验证以确保可信，但理解反例带来的洞见仍是人类数学家面临的核心挑战。