>>914

lean3から入れ子構造機能など
を加えたlean4は健全性の証明が
未証明らしい。


➖
・コラッツ予想の偽.反証の証明

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

・『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

https://arxiv.org/html/2403.14064v2