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'という定理の証明について解説しようと…
今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。前回の記事でラグランジュの定理「有限群の元の個数は部分群の源の個数で割り切れる」をLean4で形式証明しました。 maxima.hatenablog.jp 証明の肝はSubgroup.groupEquivQuotien…
今回もMathematics In Lean 4の第8章 群と環 から8.1.3 部分群を読んでいます。 8.1.3のハイライトはラグランジュの定理です。 ラグランジュの定理：有限群の部分群の位数はもとの群の位数の約数である。 |G|=[G:G'] |G'| 、あるいは同じことだが、|G|=|G/G'…
Mathematics In Lean 4の第8章 群と環 に進みます。今回は8.1.3 部分群を読んでみます。 あるタイプAの元の集合が群をなすことを示すにはGroup A、Aの元の集合の部分集合がAの演算で群をなす（部分群になる）ことを示すにはSubgroup Aと書きます。演算が加法…
Mathematics In Lean 4の第8章 群と環 に進みます。第8章ではこれらの代数構造について部分集合や代数構造間の写像をLean4で表現する方法を学びます。代数構造としてはより単純なモノイドも扱います。演算の言葉として加法や乗法が出てきますが、主に記号の…
Mathematics in Lean4を読んでいます。第7章1節で環の定義のあたりを勉強しています。前回は半群、モノイド、群などを定義し、また環の定義に備えて、乗法モノイドの性質を加法群に自動変換する方法なども説明しました。 ここまでくれば環を定義することがで…
Mathematics In Leanから第7章 階層 7.1 基礎の勉強を続けます。 "At this stage we would like to move on to define rings"というあたりで、ここから環を定義していきます。 環を定義するにあたっての課題意識は環の２つの演算である加法群と乗法モノイド…
群にあってモノイドにないものは、、、そう、逆元です。モノイドにはすでに演算があり単位元があり演算は結合的でした。そこに全ての元に逆元があれば群になるわけです。 一旦前回までに定義した道具立てを再掲しておきます。 class Semigroup₂ (α : Type) e…
Mathematics In Leanから第7章 階層 7.1 基礎を勉強中です。 ここでは代数構造の階層を構成する方法を知ります。目的はその仕組みの概要を知ることで階層を使えるようになることだそうです。なので完全な理解というよりも主要な言葉や考え方などが理解できれ…
お久しぶりになってしまいました。 暑い夏の間ちょっと数学系の話題から離れていたこともありこのブログもしばらく放置してしまいました。ぼちぼち復活していきたいと思います。 今回はすこしリハビリも兼ねて最近の私の開発環境の話です。Lean4をM1 iMac, V…
前回の記事では普通の証明としてEuclideanDomainには零因子がないことを示しました。こんな感じでした。 $a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾しま…
前回疑問に思ったことはまだ解決していません。なので今回は疑問となぜそう思ったのかだけを書いておきます。 前回までの記事でgaussIntは可換環であることを示しました。またgaussIntにquotientやremainderを定義し除法の原理を示すことでEuclideanDomainと…
