はじめに
今年で2回目の参加となるアドベンドカレンダーでは、Lean4を題材にすることにしました。
ここ何年か、代数学を中心に数学の勉強をしてきました。この分野は抽象化の力が非常に強く、概念を正確に捉えることが重要です。
一方で、抽象的であるがゆえに、各所で具体化をしっかりしていかないと、実際上どこでどう使うのかがわからなくなってしまいます。
特に私の現在の仕事では統計的な概念を扱うことが多く、数学でいうと解析学や確率論の分野に近いです。
しかし、これらの具体性のあるものだけにとどまらず、抽象化をもって一段上の理解を目指したいと考えています。
そこで、Lean4を使って数学の定義や定理を形式化することにより、概念の正確な理解と具体例の両立を図りたいと思っています。
このような理由で選んだものですので、必然的に統計方面の内容が多くなるかと思います。
関連記事
前の記事「」
次の記事「Lean4のセットアップ」
そもそもLean4とは
Lean4は、Microsoft Researchが開発した定理証明支援系のプログラミング言語です。
定理証明支援系とは、数学の定義や定理をコンピュータ上で形式化し、証明を支援するためのシステムです。
Lean4は、特に以下の特徴を持っています。
- 依存型型システム: 型が値に依存することができるため、非常に強力な型付けが可能です。これにより、プログラムの正確性を高めることができます。
- 戦略的証明: 証明を構築するための戦略的なアプローチを提供し、複雑な証明を効率的に行うことができます。
- 豊富なライブラリ: 数学的な定義や定理を含む豊富なライブラリが提供されており、これを利用して効率的に形式化を進めることができます。
Lean4は、数学の研究者や教育者にとって強力なツールであり、数学の理解を深めるための新しい方法を提供しています。
まとめ
今年のアドベンドカレンダーでは、Lean4を使って数学の定義や定理を形式化し、概念の正確な理解と具体例の両立を目指します。
特に統計的な概念に焦点を当て、解析学や確率論の分野での応用を探求していきたいと考えています。
Lean4に入門しつつ、数学の理解を深める旅に皆さんと一緒に出かけられればと思います。