てらモス🌹

ポアンカレ予想の形式化が公開されたことと、コミュニティがその内容を十分検証して受け入れたことは区別して見るべきで、そこが確認できれば、HOL Lightの解析形式化の歴史の中でもかなり大きなマイルストーンになる可能性はある。 問題は、ポアンカレ予想は数学的に有名で、証明の規模も大きい。 核心がRicci flow with surgeryという解析的に重い部分（曲率の進化、ピンチング推定、特異点のコントロールなど）にある。 したがって、ポアンカレ予想のような大規模な形式化の場合、トレースの再実行自体は比較的軽いが、この形式化が本当にポアンカレ予想を正しく捉えているのかという高レベルの検証は、微分幾何 / Ricci flowに詳しく、かつ証明支援系にも通じた人でないと難しい。 しかし、LeanとHOL Light（特にHarrison系の解析証明）をおおざっぱな雰囲気で比較。こう見ると、数学者でも「読める」仕様になっている。 Lean have h₁ : ... have h₂ : ... rw [some_lemma] simp at h exact h このようにタクティクを順に適用していく手順書のような書き方になりやすい。数学的な内容を追うには、各タクティクが何をしているかをある程度理解する必要がある。 Ocaml(HOL) ε > 0 ⇒ ... ⇒ ... ⇒ |f(x) - L| < ε 含意の連鎖で書かれることが多く、ε-δ論法などの古典的な解析の書き方にかなり近い。単純型と集合論的なエンコーディングの影響もあり、証明が数学的な推論の流れとして読める形になりやすい。これは、ε-δ論法の思想を多分に受け継いでいること(特にゲージ積分などの解析ライブラリで顕著）が大きい。