DeepMind神经符号方法解决9个Erdos问题，比OpenAI更严谨

DeepMind团队使用神经符号方法（neurosymbolic）成功解决了9个开放的Erdos问题，工作比OpenAI更细致、定量化。该方法结合了LLM和Lean证明助手，实现自主推理，仅在形式验证通过后才进行人工审核。Gary Marcus评论称，OpenAI可能因知道DeepMind即将发布而仓促推出自己的方案。这一进展展示了神经符号方法在数学推理中的潜力，也引发了关于研究竞争和严谨性的讨论。