課題と今後の展望

ファイルフォーマット

エクスポートファイルのフォーマットをJSONに移行する件について、こちら にオープンなRFCがあります。これは大きなバージョン変更になるでしょう。

整数・文字列が適切に定義されていることの確認

Nat・String・およびそれらに関連するカーネル拡張がカバーする操作のためのエクスポートファイルの宣言が、信頼されたコードにエクスポータを引き込まない方法で拡張が期待するものと一致するかどうかを判断するための特定の解決策について Lean コミュニティはまだ定まっていません。

Eq と Quot の宣言のようなアプローチ（型チェッカ内で手作業で定義し、それらが同じであることを保証する）は Nat でサポートしているバイナリ演算のための完全にエラボレートされた項が複雑であるため実行不可能です。

Pollack consistency の改善

Lean 4 はカスタム構文・マクロ・プリティプリンタの定義に非常に強力な機能を提供し、Lean 4 の内部のほとんどすべての側面がユーザによって利用可能です。Lean の設計のこれらの要素は Lean 3 の存続期間中に mathlib コミュニティから実際に寄せられたフィードバックに対する効果的な対応でした。

これらの機能は大規模な形式化作業を可能にするツールとして Lean が成功した重要な要因である一方、Lean 4 の Pollack consistency¹ が危うく、もしくは損なわれる恐れがあります。プリティプリンタでマクロと構文拡張機能を複製しなければ、型チェッカは一貫して項を認識可能な形で読んでユーザに返すことができません。しかし、これらの機能をプリティプリンタに追加するアイデアは信頼されたコードベースを拡張する点においては魅力的なものではありません。別のアプローチとしてプリティプリンタをやめて、信頼できるパーサ（通称 metamath zero）を採用する方法もありますが、Lean のパーサはカスタム構文宣言を使ってユーザ空間でその場で変更することができます。

Lean が成熟し、採用が進むにつれて Pollack consistency を犠牲にすることなく、ユーザが Lean の拡張性を活用できるような技術や手法の開発が進められるでしょう。

前方推論

既存の型チェッカは後方推論の形式を実装しています；型チェッカの戦略の別路線として、外部プログラムによって作成された前方推論の連鎖を受け入れ、チェックすることがあり、これは後方推論よりもシンプルな型チェッカとなる可能性があります。