証明とリーズニングとLean

Lean 半形式証明スクリプト 論理
一般 抽象的 Lean 具体的
ライブラリコンテキスト プレリュードとインストールしたパッケージ達
ワーキングコンテキスト モジュール／名前空間／セクションのコンテキスト
質問コンテキスト 未証明定理の前提
判断コンテキスト 既証明定理の前提