Lean4+Mathlib4の組み合わせで証明が出来上がるとレポジトリをGithubで公開したくなります。この時にGithub Actionsを使ってCI (Continuous Integration)を設定しておくと、利用者がレポジトリをダウンロードしてから利用を開始する体験を向上できます。この…

以前ワンタイムパッド暗号を紹介し、その完全秘匿性をLean4で形式証明しました。暗号の定義の中で「使った鍵は再利用してはいけない」、ということを書きました。ただしその条件は証明の中で明示的に使われているようには見えないし、数学的な条件なのか一般…

最近の記事では暗号とその安全性証明の基礎を勉強したいと思い、シャノンの完全秘匿性やそれを実装するワンタイムパッド暗号、完全秘匿性を持つ暗号における鍵の長さに関する定理の証明などを勉強しました。安永さん（東工大の先生ですね）の本を購入し、ま…

今回は完全秘匿性の話題に戻り、シャノンの論文でも証明されている、鍵の集合$K$と平文の集合$M$の大きさに関する定理をLean4で形式化して証明します。 https://tcc.c.titech.ac.jp/yasunaga/appmath6/perfect.pdf では定理６として述べられている次の定理で…

シャノンが暗号に関する論文で「完全秘匿性」という概念を定式化したことを紹介し、そのLean4での形式化までを前回の記事で紹介しました。 この概念がただの抽象概念で、そのような性質を満たす暗号など簡単には作れない、、、という話かというとそうではあ…

完全秘匿性という概念、せっかく数学的に定義したのですが数式が出てこないと数学している気分になれません。というわけで暗号の完全秘匿性について数式を用いて定義してみましょう。また数式化できればLean4での形式化も見たいですよね。とは言っても暗号と…

これから数回にわたって「セキュリティを数学的に証明する」話を書いていきます。自分の勉強のための覚書みたいなものですし、まだ勉強を始めたばかりの分野なので記載に間違いがあるかもしれません。そもそも理解の方向性が間違っているかもしれません。決…

今日はちょっと別件でネット検索していたらびっくりすることに気がつきました。 テレンスタオ教授（フィールズ賞受賞者、UCLA）が２週間ほど前からユーチューブを始めていて、3本の動画を投稿されています。全部、Lean4の使い方ビデオでした。 www.youtube.c…

前回はコインを2回投げる試行のPMF（確率質量関数）による記述方法を紹介し、2回とも同じ面がでる確率事象の記述の仕方と確率を証明しました。 今回は同じように2回投げる試行で2回とも表が出る確率事象の記述を行い、その確率が1/4であることを証明します。…

前回の記事ではLean4での離散確率の形式化としてPMF (Probability Mass Function, 確率質量関数)について紹介し、コイントスをPMFで記述して、表や裏が出る確率が1/2であることを証明しました。 今回はコインを2回投げる試行のPMFによる記述方法を紹介し、い…

少し事情があって?Lean4での確率の取り扱いについて勉強をしています。とは言っても決して本格的な確率論(測度論をベースにした確率密度関数や確率分布など)ではなく、算数や中学校で習うレベルの確率の話です。いわゆるコイントスの確率やサイコロの確率な…

Mathematics in Leanを読んできましたが、今回を最終回とします。11.1. Elementary Differential Calculusと12.1. Elementary Integrationの内容の紹介です。 import Mathlib open Real-- サイン関数を微分するとコサイン関数example : deriv sin = cos := b…

今日は3月14日、毎年恒例の円周率の日です。 今年はなんと満月なんです。今、まだ今夜の満月を見ていない人、すぐに外に出てください。関東地方は晴れていて見られます。 記念に今夜のお月様を撮って見ました。次に円周率の日に満月が見られるのはいつのこと…

少し複雑な関数の極限として $$\lim_{x\to 0}x\,\sin{\frac1{x}}=0$$ を証明します。$x$が$\sin$の引数の分母にあるので$x=0$では定義されませんが$x\to 0$での極限は存在して$0$になる、という命題です。 今回は関数の絶対値を取ってから挟み撃ち論法で証明…

今回は関数の極限の証明を見ていきます。 $$\lim_{x\to 2} 2\,x = 4\hspace{20cm}$$ example : Tendsto (fun x:ℝ => 2*x) (𝓝 2) (𝓝 4) := by have cont_two_mul : Continuous (fun x : ℝ => 2 * x) := by exact continuous_const.mul continuous_id refine C…

まずは数列の極限の証明を見て見ましょう。 $$\lim_{n\to\infty}n = \infty\hspace{20cm}$$ example : Tendsto (fun n:ℕ => n) atTop atTop := by exact tendsto_id exact一発で終わるということは全く同じか、より一般化された証明があるということです。こ…

Mathematics in Lean 4も最後の方に辿り着きつつあります。これから数回にわたってLean4による解析学の証明を見ていきます。Mathematics In Lean 4の章立てで言えば10.1 Filtersあたりなのですが、そこでの扱いはもっとはるかに抽象的です。この記事では具体…

久しぶりに（このブログのタイトルにもなっている）Maximaの話題です。 Maximaをブラウザの中でローカルに動かすことに成功しているようです。 https://maxima-on-wasm.pages.dev/ にChromeなどのブラウザでアクセスするとMaximaが起動した画面が表示されま…

前回の記事 -数学- Lean4のお勉強 ラグランジュの定理の続き - Maxima で綴る数学の旅 は色々と修正するべき点や補おう点があり、ここに書き直すことにしました。 前回はGを群、G'をその部分群としてG ≃ (G ⧸ G') × G'という定理の証明について解説しようと…