証明テンプレート

Leanに限らず、どんな証明系でも定理ライブラリの構築は熱心。Leanだと自動化タクティクのライブラリも整備されるだろう。

だが、特定パターンの証明のやり方をガイダンスするテンプレートみたいなものはない。定型文書作成のテンプレートと同じで、穴埋めすると完全な証明が出来上がるようなヤツ。

現実の証明では、こういう証明テンプレートが暗黙に使われていると思うのだが。