Mathematics in Lean4 もいよいよ第6章まできました。「6.1 構造の定義」は今までの知識があればとても簡単に読み進むことができました。いわゆるレコード型のような構造およびそのレコード型に付随する関数（演算）、そしてレコード型の各フィールドあるい…

連休直前の４月２９日より、イギリスでは消費者向けの様々なIoT機器（みなさんがよく使っているスマホ・スマートテレビ・スマートスピーカーを含むおよそ全てのネット接続機器）に一定のセキュリティ対策が施されて販売されています。 非常に大雑把に言うと…