コラッツ予想のAI反証が3日で崩れた原因と再発を防ぐ点検ポイント

A soundness bug in the Lean kernel ( #14576 ) was reported and fixed during the week of July 27. ／ On July 25, Ramana Kumar published a repository containing a sorry -free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576 . We pushed a fix one hour after the report ( #14577 ). Joachim Breitner reviewed it and suggested improvements, and it was merged. New patch releases are out. — 発生から修正までの経緯に関する記述より

The bug: when the kernel eliminates a nested occurrence under an inductive type T with parameters Ds , and these parameters are phantom (not mentioned in constructor fields), they disappear from the generated auxiliary type and thus escape type checking. An ill-typed argument in that position could be used to make the kernel accept a proof of False . The bug is only reachable through metaprogramming, by sending the inductive declaration to the kernel directly. The frontend checks the arguments and catches the ill-typed term. This is an implementation bug, not a hole in Lean's meta-theory. — バグの技術的内容、到達経路、および位置づけに関する記述より

One suggestion in the discussion is to remove or restrict metaprogramming so that this attack is not expressible. This is misguided. The elaborator is untrusted by design. Soundness cannot depend on an untrusted component refusing to build a bad term. An attacker who wants to submit a malicious proof can also write .olean files directly or modify memory, both of which bypass the elaborator entirely. The kernel has to reject ill-typed declarations on its own, in its own process. This separation and isolation of concerns is one of the main advantages of proof terms. — メタプログラミング制限案に対する見解より

The original Collatz repository also passed a week-old version of nanoda , the main external checker. nanoda is an independent kernel (aka proof/type checker) for Lean implemented in Rust by Chris Bailey . The surprising part is that there are two unrelated bugs involved. The official kernel had a missing check in the nested inductive type support, as explained above. nanoda did check that spot, but did not verify the type name in a projection node. The nanoda bug was reported by Jeremy Chen and fixed a week before the Lean bug was reported. ／ The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both. ／ lean4lean is affected by the kernel bug, since its handling of inductives is a port of the reference implementation. — 独立検証器 nanoda がすり抜けた理由、独立カーネルによる検証が依然有効である理由、および lean4lean への影響に関する記述より

The proof was built so that the expression the kernel never inspects is one that the old nanoda accepted. ／ Ramana believes the timing was coincidental, but cannot rule out that the model had seen the nanoda report. Joachim proposed the hypothesis that the timing coincidence is due to the availability of strong models able to find this bug. — 証明が狙っていた箇所、および時期の一致についての当事者の見解より

Regression tests for the exploit, and for a related non-uniform-parameter case raised by Arthur Adjedj, are in the Kernel Arena . ／ A follow-up PR ( #14582 ) makes the kernel check that the parameters of a nested occurrence actually behave as parameters, rather than only re-type-checking them. ／ We have also hardened kernel invariants. PRs: #14621 , #14631 , #14632 . — 回帰テスト、追加検査、およびカーネル不変条件の強化に関する記述より

Daniel Selsam at OpenAI assisted the Lean FRO with an AI specialized in cybersecurity, and found other programming mistakes in the Lean kernel. All of them have been fixed. All of them were caught by nanoda. These bugs are also only reachable through metaprogramming. PRs: #14607 , #14608 , #14609 , #14613 , #14615 , #14616 . ／ comparator.live now runs nanoda by default, and nanoda is tracked daily so lean-eval and comparator stay current after upstream fixes. — OpenAI の協力による追加のバグ発見と、検証環境側の更新に関する記述より

#14807 fix: make the kernel is_prop check require a sort and #14843 fix: apply #14807 fix to inductive.h. These two PRs fix the implementation of the function that decides whether a type is a proposition. The bogus proof was accepted by nanoda. ／ The following PRs do not fix soundness bugs. ／ #14607 fix: missing check_no_metavar_no_fvar checks at inductive.cpp. ／ #14608 fix: check universe parameters in mutual definitions. ／ #14609 fix: mark exported stubs of partial definitions as unsafe. ／ #14615 fix: decide inductive predicates up to universe normalization. — 続報での健全性バグとそうでない修正の区分に関する記述より

Mario Carneiro's lean4lean is a Lean formalization of Lean's type theory together with a proof that the kernel implements it. The work is ongoing, the proof of consistency does not cover inductive types yet, and the to-be-verified implementation suffered from the same bug as the official kernel. The bug would have been found when attempting to conclude the verification of this part. — lean4lean による検証の進捗に関する記述より