敵対的な入力

より一般的な信頼の問題に対してしばしば付随するトピックとして、敵対的な入力に対する Lean の堅牢性が挙げられます。

正しい型チェッカは利用者が許可する公理のもとにおいて、受け取る入力を Lean の型システムのルールで制限します。利用者が許容する公理を3つの「公式の」公理（propext・Quot.sound・Classical.choice）に制限した場合、入力ファイルはどのような状況においても型チェッカが受け入れる prelude の False である証明を提供することはできないはずです。

しかし、最小の型チェッカは論理的には正しいですが、利用者を欺くように設計された Lean の宣言を提供する入力から積極的に保護することはできません。例えば、敵が深い依存関係を理解した上で再定義してレフェリーが検査しないようにしたり、ユニコードに似たものでプリティプリンタの出力を生成するようなものを導入しつつその裏で重要な定義変更をしたりできてしまいます。

「ある定理が形式的に証明されたとユーザが考える一方で、実際にはシステムが実際に行ったことが何であるかについてユーザが誤解している」というアイデアは Pollack consistency という概念で扱われており、Freek Wiedijk によるこの書籍¹ で議論されています。

このようなカーネルの最小限の機能でカバーできない攻撃に対する保護を提供するために、開発者がソフトウェアを書いたり、型チェッカを拡張したりすることは原理的に妨げるものは何もありません。しかし、Lean のユーザがその強力なカスタム構文とマクロシステムをどの程度まで受け入れているか、ここまでの話を改善することに興味を持つ人々にとっていくつかの課題が生じる可能性があります。読者におかれましては、このことを多少なりとも 今後の課題 として考えるべきでしょう。