ほんまやね。まぁそのうち証明されるやろけど。たぶん純理論的には問題ない。一部残ってるかもしれないヒューマンエラーが洗い出されれば安心して使えるでしょ。Lean の基礎理論(数学部分)とコーディング部分の正当性を Lean に検証させるプロジェクトも実行中らしいし。それが通ったらもう信頼性はほぼ完ぺきになるやろな。