Maxima で綴る数学の旅

紙と鉛筆の代わりに、数式処理システムMaxima / Macsyma を使って、数学を楽しみましょう

-数学- Lean4のお勉強 シュレーダー=ベルンシュタインの定理

第4章「集合と関数」の最後のセクションはシュレーダー=ベルンシュタインの定理のLean4による証明です。 初めてこの定理をきちんとした形で知りました。集合論の濃度に関する基本的な定理です。 定理:$\alpha, \beta$を集合、$f:\alpha \rightarrow\beta, …

-数学- Lean4のお勉強 関数

Mathematics in Leanの第4章「集合と関数」の中の2つ目のセクションである「関数」を読みながら練習問題を解いています。その問題の中で集合族の積集合の写像と集合族の写像の積集合に関する問題がありました。全称量化子と存在量化子が絡み、なかなか手強…

-その他- macOSとbluetooth イヤフォンの現状と音質の改善方法

しばらく前のmacOSではbluetoothイヤフォンで音楽を楽しむ際、コーデック選択の問題で音質が悪い状況がありました。私もiMacとソニーのWF-1000MX4 の組み合わせでこの辺について色々と試してきています。 最近知ったのですが、この状況は少なくともmacOS Son…

-数学- Lean4のお勉強 集合を扱う

Mathematics in LeanもC04 Sets and Functionsの最初の章である集合まで辿り着きました。ここでは集合に関する性質の証明方法のLean4での実現の仕方を知ります。 集合が等しいこと(A=B)を示す場合、ゴールをA=Bとして方法として、AがBの部分集合であり、かつ…

-数学- Lean4のお勉強 関数型言語が証明に顔をだす

Lean4を証明支援系として使っていても、型と証明の対応や関数型言語が突然現れることがあります。このことを知っていないと証明が読めないことがありました。 具体的には例えばある定理がこんな形だったとします。 def P (x:ℕ) : Prop := sorrytheorem theoA…

-数学- Lean4のお勉強 論理積∧ と 論理和∨

Lean4での論理記号の取り扱いの勉強も後半です。今回は論理積と論理和の扱いを見ていきます。この辺はあまり難しい話は出てきません。 ゴールが論理積A ∧ Bの形の場合にはconstructorタクティクを使うとAとBが両方ともゴールとなり両方証明するとA ∧ Bの証明…

-数学- Lean4のお勉強 否定

否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク:ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ B…

-数学- Lean4のお勉強 タオ教授のブログより

現役で最高の数学者のお一人で情報発信にも熱心なテレンスタオ教授のブログがあります。 terrytao.wordpress.com 残念ながら難しすぎて普段はほとんど見ない数学ブログですが、Lean4の勉強をしていたら検索で記事が1つヒットしました! A slightly longer L…

-数学- Lean4のお勉強  存在量化子 ∃

ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by us…

-数学- Lean4のお勉強  全称量化子 ∀

今勉強しているMILの第3章「論理」では仮定の論理式やゴールの論理式に登場する論理記号をタクティクでどのように取り扱えば良いのかを説明しています。 この章の最初の方で説明されるのは全称量化子 ∀ です。ゴールの論理式にこの論理記号がついている場合…

-数学- Lean4のお勉強 calcモード

前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しま…

-数学- Lean4のお勉強で使っている環境

数学の記事では普通は環境について書かないのですが、Lean4はプログラミング環境でもあるし、一応概要を記しておきます。 パソコン:M1 iMac (主記憶16GB), macOS 14.2.1 Lean (version 4.5.0-rc1) VS Code バージョン1.85.1 VS Code機能拡張Lean4 v0.0.124 …

-数学- Lean4のお勉強 証明支援、applyタクティク、have

"Mathematics In Lean"に沿ってLean4の証明支援系の勉強を進めています。まだ基本編で、今やっているのはmin, maxの性質の証明です。具体的には全順序集合上の関数min a b (a, bの小さい方を返す)について次の性質の証明です。 min a (min b c) = min (min…

-数学- Lean4のお勉強 証明支援、rw, applyタクティク

これからしばらくの間はLean4の証明支援系の勉強の話をシリーズ的に記事にします。相変わらず自分の勉強メモのような感じです。つまづいたところや感動したところを中心に書いていきます。 使用するテキストはMathematics In Lean(通称MIL)にしました。 Math…

-数学- Lean4のお勉強 関数型プログラミング

年末は帰省していたのですが、有休含めて1/8までお休みにしたこともあり時間ができました。そこでLean 4を勉強してみることにしました。 Lean 4は以前このブログで紹介したLean 3と呼ばれる定理証明支援システムの後継システムです。 Lean 4からは関数型プロ…

-セキュリティ- CISSP練習問題を量産する

今年もこのブログをよろしくお願いします。 昨年の12月に最初は数日おきに、途中から毎日CISSPの練習問題を作成して投稿する、という企画を実行してみました。 CISSP資格試験の問題は巨大なテスト問題のバンクからほぼランダムに選んで各受験者に対して出題…

-セキュリティ- コントロールのタイプ CISSP練習問題 ドメイン1

今回が「CISSP練習問題」の最終回です。途中からアドベントカレンダー風に毎日投稿してきました。ただコントロールの話はぜひ出題したいと思っていて、クリスマスをはみ出して投稿を続けていました。 最終回はセキュリティコントロールの5つのタイプの分類…

-セキュリティ- 管理コントロール CISSP練習問題 ドメイン2

情報セキュリティのコントロールの3つの種類に関する問題です。この話はドメイン1に書かれるべきだと思うのですが、データセキュリティと絡めてドメイン2に書かれています。 管理コントロール(Administrative Control)は何を使用して組織の資産を守りますか…

-セキュリティ- ASLR CISSP練習問題 ドメイン3

ドメイン3からASLRの効果に関する問題を出題します。 攻撃者が自身のテストマシンで成功した悪用コードを対象システムで実行する際のASLR(Address Space Layout Randomization)の影響は何ですか? a. 悪用コードが失敗する可能性が高まる b. セキュリティポ…

-セキュリティ- ブロック暗号モード CISSP練習問題 ドメイン3

暗号に関してはCBKにも結構専門的なことが記載されています。ここは頑張って勉強しなければなりません。 カウンター(CTR)モードの主な特徴は何ですか? a. フィードバックに前の暗号文を使用する b. 同じ平文は同じ暗号文を生成する c. 同じ平文は同じ暗号…

-セキュリティ- リスク対応 CISSP練習問題 ドメイン1

アドベントカレンダーはクリスマスまでのものですが、このシリーズは12月28日までは続けようと思います。 ドメイン1からの出題です。リスクが識別されて分析・評価された後に組織としての対応を決める必要があります。このリスク対応に関する問題です。 特定…

-セキュリティ- パッチ管理 CISSP練習問題 ドメイン7

ドメイン7はセキュリティ運用に関するドメインです。すでにそれ以前のドメインで紹介されているセキュリティの概念やシステムを現場で運用する方法を述べています。パッチもドメイン3やドメイン6ですでに部分的に述べられています。ドメイン7では脆弱性管理…

-セキュリティ- LDAP CISSP練習問題 ドメイン5

個人的の感想ですが、ドメイン5は割とタフで勉強が大変な印象です。IAAAの基本概念、ID連携、シングルサインオン、LDAP, Kerberos, RADIUS, SAML, OAuthなど認証/認可のシステム、MAC, DAC, RBAC, ABACなどの認可の仕組み、type1〜3 の認証要素、ID管理とラ…

-セキュリティ- ID連携 CISSP練習問題 ドメイン5

ドメイン5からフェデレーテッドアイデンティティ(ID連携)に関する問題を出します。 フェデレーテッドアイデンティティ管理(FIM)においてセキュリティ専門家が検討すべき重要な要素は? a. フェデレーションのビジネス利益 b. アイデンティティ管理の複雑性…

-セキュリティ- データ分類 CISSP練習問題 ドメイン2

ドメイン2からデータ分類に関する問題です。データ分類は地味ですが重要なセキュリティ施策です。 データ分類ポリシーと手順を持つことは、情報を最も効率的かつ効果的に保護するためのどの段階で役立ちますか? a. データの分類を行う前 b. データの分類中…

-セキュリティ- IoTセキュリティ CISSP練習問題 ドメイン3

CISSPのCBK (Common Body of Knowledge)のドメイン3には新しい技術もいくつか記載されておりIoT機器も取り上げられています。今回はそのIoT機器のセキュリティの問題です。 セキュリティ専門家がIoTデバイスの脆弱性を評価する際、最も重要な要因は何でしょ…

-セキュリティ- 組織とセキュリティ CISSP練習問題 ドメイン1

もう一問ドメイン1から出題します。現代では組織をつくり社会的な活動をするときには最初からセキュリティを考慮する必要があります。それを実際にやり始めるにはどうしたら良いか、考えてみて下さい。 組織にセキュリティ機能を実装する際にトップダウンア…

-セキュリティ- セキュリティの目的 CISSP練習問題 ドメイン1

ドメイン1からの設問です。組織の中でのセキュリティ機能の位置付けに関する問題です。 セキュリティガバナンスにおいて、組織が最も行うべき活動には次のうちどれが含まれますか? a. 組織のセキュリティ機能を特定のプロジェクトにのみ適用すること b. 組…

-セキュリティ- CIA CISSP練習問題 ドメイン1

ドメイン1からの出題です。情報セキュリティにおいて最も基本となる概念であるCIAに関する問題です。 情報が正確であること、妥当であること、および欠落がないこと、を維持する概念は何ですか? a. 完全性 b. 可用性 c. 信頼性 d. 機密性 正解:a 完全性 …

-セキュリティ- SDLC CISSP練習問題 ドメイン8

ソフトウェアの開発を理解しその中で必要なセキュリティ対策を実施していくことは非常に重要です。 SDLCのどのフェーズで、システムの要件が文書化され、システムの設計と必要なアーキテクチャが行われますか? a. 初期化 b. 開発 c. 配備と納品 d. 運用と保…