Masahiro Sakai

ホルムズ海峡閉鎖なら世界経済に打撃　日本は原油9割を中東に依存：朝日新聞 米国とイスラエルのイラン攻撃で懸念が高まっているのがイランによるホルムズ海峡の封鎖だ。世界の海上エネルギー輸送の「大動脈」であり、もし実際に封鎖となれば、原油価格の高騰や世界経済への打撃は避けられな…

有料記事がプレゼントされました！ 3月1日 18:13まで全文お読みいただけます。
ホルムズ海峡閉鎖なら世界経済に打撃　日本は原油9割を中東に依存：朝日新聞
digital.asahi.com/articles/ASV...
これもどうぞ

【そもそも解説】なぜ米国とイスラエルがイラン攻撃　7つのポイント：朝日新聞 米国とイスラエルが中東の地域大国イランへの軍事攻撃に踏み切った。なぜ今だったのか、今後起きうる事態はどのようなものか。押さえておきたいポイントをQ＆A形式でお届けします。■①米国とイスラエルは、なぜ…

有料記事がプレゼントされました！ 3月1日 18:12まで全文お読みいただけます。
【そもそも解説】なぜ米国とイスラエルがイラン攻撃　7つのポイント：朝日新聞
digital.asahi.com/articles/ASV...
よかったらどうぞ　わたしはこれから地図帳でも買って帰ろうかなあと思ってるところ

Bambu Lab A1 mini のノズルが詰まってしまったぽくて、困ってしまったが、 wiki.bambulab.com/en/a1-mini/t... を参考に色々やっていたら直ったっぽい。

2/27(金)から花粉症の症状（倦怠感、目鼻喉の痛痒みと痛み、頭痛、etc.）がひどくて死んでいる……

Live Updates: U.S. and Israel Conduct Strikes on Iran

今度はイランで戦争が始まる。第1報を記録

New York Times
www.nytimes.com/live/2026/02...
2月28日、米国とイスラエルがイランを攻撃。

複数の住民が、イランの首都テヘランで大規模な爆発を報告。テヘラン市民は、大統領宮殿と国家安全保障会議がある地区から煙が立ち上るのを見たと報告。

イランの準公式通信社ファルスによると、他の都市でも爆発音が確認された。同通信社はコム、ケルマーンシャー、イスファハーン、カラジで爆発が起きたと報じた。

米軍は、同地域に空母2隻、駆逐艦複数隻、戦闘機50機以上を配備。
（続く

「ゼロから始めるLean言語入門」の「3.5 選択原理」を読んでいて、関数の全射性から右逆関数を構築できないことにちょっと驚く。 Lean の ∃ は Σ-型 とは別の型で、Propにしかeliminateできないのか。また、LeanではPropはTypeの階層とは別扱いで、Typeに埋め込むにはPLiftというのを使うらしい。

Modeling Assistant: Tool execution failed Reached max attempts (10) without passing jm-check: Code execution timed out. Please check for infinite loops or reduce computation complexity. Auto: I apologize for the delay. Due to the complexity of the [redacted], the automated code generation timed out. I have manually prepared the JijModeling code and the parameter extraction script for you.

JijZept AI を試してたら、こんなの出てきた。

ツールとして呼び出している Modeling Assistant が失敗続きで、メインのエージェントが、痺れを切らして、自分で実装したってこと?

ユーザーからしたらどちらも自動なのに、しかもAutoという名前のAIが、manuallyと言っててちょっと面白かった。

Noeon Research Noeon Research is a startup conducting research on the architecture that is an alternative to Transformers-based ones. The company’s goal is to build an AI system for automated code processing for com...

先週から Noeon Research という会社で Data Structure & Algorithm Engineer として働き始めました。会社のメンバーページに掲載されたので、このタイミングでご報告まで。今後ともよろしくお願いします！
noeon.ai/team/

macOSのデスクトップアイコンはなぜ右寄せなのかを考える｜usagimaru 左横書きのインターフェイスでは画面の左側を「上手（かみて）」とし、左上から右下に向かって情報と時間が展開していくような形をとります。ですから、macOSのデスクトップアイコンが伝統的に右寄せ・縦並びの配置を採用することは、日本語の縦書きを想定するならまだしも、英語の左横書きを前提とするインターフェイスとしてはとても不思議な光景です。WindowsやiOSでは左寄せが基本ですから、ある意味でMacの...

macOSのデスクトップアイコンはなぜ右寄せなのかを考える note.com/usagimaruma/... 👀

外国遺族年金への課税「平等原則に違反しない」 東京地裁が請求棄却：朝日新聞 日本の遺族年金は非課税なのに、外国の遺族年金には相続税がかかるのは不公平――。そんな論点を巡って争われた裁判の判決が25日、東京地裁であった。篠田賢治裁判長は、外国の遺族年金への課税は「合理性を欠く…

これ気づいてなかった！国外遺族年金に相続税課税するやつ国側が勝ってしまったのか！😱

有料記事がプレゼントされました:
digital.asahi.com/articles/ASV...

ryoppippi on X: "自分をhiringしようとしていた会社が、hiringに失敗した後に俺のOSSから実装をコピーしてcreditを消して公開していた件について １ヶ月くらい調査してたけどどっかでblogを書くと思う 厚顔無恥にも程がある" / X 自分をhiringしようとしていた会社が、hiringに失敗した後に俺のOSSから実装をコピーしてcreditを消して公開していた件について １ヶ月くらい調査してたけどどっかでblogを書くと思う 厚顔無恥にも程がある

この話が気になるが……
x.com/ryoppippi/st...

へぇ、こんな会社があったんだ。 “Symbolica is an artificial intelligence research lab that is pioneering the application of category theory and type theory to build a symbolic reasoning engine.”
www.symbolica.ai

MN-Core Technology Conference 25を開催しました。 - Preferred Networks Tech Blog はじめに 昨年、2025年12月16日にMN-Coreにまつわるイベント 「MN-Core Technology Conference 25」

MN-Core Technology Conference 25 開催レポートをやっと読めた。
tech.preferred.jp/ja/blog/mn-c...

会社(ウォンテッドリー)のチーム研鑽用予算で、ラムダノートの本をありったけ買いました。
みんなに読んで最強になってもらおうと思います。

ゼロから始めるLean言語入門、evalでPropがboolに評価されたり、命題外延性（propositional extensionality） (P ↔ Q) → (P = Q) が仮定されていたりと、型理論的にどういう体系になってるのか気になって来たぞ。

天皇陛下∩( ・ω・)∩ばんじゃーい

ゼロから始めるLean言語入門、コード3.19で case という知らないタクティックが出てきた。あと、直前でゴールが複数ある場合には最初のゴールに集中する「·」(centor dot)を使うのが良い書き方だとあったけど、ここでは使われておらず、caseを使う場合にはcase自体に「·」が含まれている感じ?

結果発表 100点 受験番号：005835 2026年度 合格通知書 本屋大学 あなたの得点100点 合格おめでとうございます。 あなたは2026年度本学入学試験に合格されましたので、ここに通知します。

抽選で丸善ジュンク堂書店専用QUOカードPayが当たる本屋大学入試挑戦キャンペーン www.maruzenjunkudo.co.jp/pages/cp-000... むずっ！ 調べまくって一応全問正解したけど。

BlackHole: Route Audio Between Apps Zero Latency. Perfect for Streamers, Podcasters, and Online Instructors.

音声データは、プレイヤーで再生したものを、 macOS 用のループバックドライバの BlackHole を使って録音してみた。便利だね。 $10寄付。
existential.audio/blackhole/

Backblaze バックアップソフト 1年版 Backblazeとは1日わずか11円。容量無制限だから外付けHDDもまとめてバックアップ「Backblaze」は、インストールするだけでパソコンのデータを容量無制限で全自動バックアップできる画期的なサービスです。

と思ったら、割引率がアップして復活してた。2/27 まで 73% オフ (￥14,960 → ￥3,980)。とりあえず3年分くらい買っておくか。
www.sourcenext.com/product/0000...

年収2500万でも貧困層？ 米マイクロソフトに18年勤務した日本人エンジニアが「日本は健全」と語るワケ - エンジニアtype | 転職type 米マイクロソフトに18年勤務し、プリンシパル級まで登り詰めた日本人エンジニアを襲った「5分間の解雇通告」。年収2500万円でも低所得とされる米国の異常な物価、30分の手術で2250万円の請求……。行き過ぎた資本主義の最前線を見た彼が、絶望の先に見つけた「日本の健全さ」とエンジニアの真の幸せを問う約1万字のロングインタビュー。

ほー、と思って読み進めたらBlueskyで馴染みの方のインタビューだった

type.jp/et/feature/3...

Rustで学ぶWebAssembly Interface Type入門

Rustで学ぶWebAssembly Interface Type入門 zenn.dev/chikoski/art... 👀

DLL Hell から .NET の自己完結型デプロイまで：30年の依存関係戦争

DLL Hell から .NET の自己完結型デプロイまで：30年の依存関係戦争 zenn.dev/takekazuomi/... 👀

www.stephendiehl.com/posts/lean-o... を翻訳したら、「ます」が「〼」になって、どういうことかと思ったら、 font-feature-settings に "dlig" (Discretionary Ligatures) が含まれていて、ヒラギノ明朝には江戸時代の略字の名残として、送り仮名の「ます」を「〼」に変換するリガチャが含まれているかららしい。おもしろ。

移動中にタブレットからリモートのvscodeに繋いでLeanを使えないかなぁと思って VSCode Remote Tunnels を試して見たら、 Lean Infoview は出るけど Lean Infoview の更新中のクルクルがずっと回ったままだな。 Remote Tunnels 経由だと使えないのかな……

Leanで #check MyNat.succ .zero の結果が MyNat.zero.succ : MyNat になるのは、第一引数をレシーバとしたOOP的な表記になってるのかな。

I completed the ‎February challenge‎ faster than ‎93.7‎% of all learners on Duolingo!

今年も PB のコンペ開催されるそう。

Pseudo-Boolean Competition 2026
www.cril.univ-artois.fr/PB26/

音声も追加できた（BGMは別のものに差し替えたけど）。 ゲームとかで音声を再生するには、HTML5のaudio要素ではなく、 Web Audio API というのを使うと良いようだ。

第28回プログラミングおよびプログラミング言語ワークショップ（PPL 2026） プログラム jssst-ppl.org/workshop/202... 👀