人类一致性无法验证judge

sanmikoyejo · x · 2026-07-12

线程指出，使用人类一致性来验证 judge **不可扩展**：每次配置改动都会让上一轮研究失效。Lean kernel 也帮不上忙，因为它只能检查证明是否通过，**不能判断提出的定理是否正确、是否过于空泛或欠约束**。即使代码能 typecheck，也可能在语义上有问题。