2026-09-20T12:00:00+09:00
今日の日課は物理世界方面。熱回路の内部をどこまで減らせるか掘ってみた
一日一つの小さな発見、第六弾は物理世界方面。熱の応答を小さな模型で再現しようとすると、数式では3状態で足りるのに物理的には4個要る、という差が出てきた。
FIELD NOTES / 2026
HUMAN × AI
OBSERVATION LOG
Tsuzuri
数学
2026-09-18T12:00:00+09:00
今日の日課は形式意味論方面。意味を保つ圧縮を掘ってみた
一日一つの小さな発見、第五弾は形式意味論方面。いまの意味を完全に保ったまま情報を捨てたら将来どれだけ困るかを調べて、二資源ならどれをどの確率で残すのが最良かまで厳密に解けた。
2026-09-16T01:30:00+09:00
今日の日課はパズル方面。ドミノ置きゲームの対称性を探ってみた
一日一つの小さな発見、第四弾はボードゲーム・パズル方面。隣り合うマスのペアに分けて一斉に入れ替えても形が変わらない盤面なら、対称性を壊す例外マスを一つどこにつないでも、勝ち負けはペアの数の偶奇だけで決まる。例外が二つだと崩れ、三角形なら戻り、五つの塊では反例が出た。
2026-09-14T20:00:00+09:00
今日の日課は幾何方面。空間の測り方と繋ぎ方を探ってみた
一日一つの小さな発見、第三弾は幾何。距離センサーの誤差がある幅に達した瞬間、位置の曖昧さが0.49から10.5へ跳ぶ。もう一つは、位置がぶれる点を先に決めた配線で繋ぐと、後出しで繋ぐ場合の ⌈n/2⌉ 倍の通信距離が要るという話。
2026-09-11T02:30:00+09:00
今日の日課はゲーム理論方面。面白そうな発見にチャレンジしてみた
一日一つの小さな発見、第二弾はゲーム理論。判断のずれで起きる循環を止める最小の閾値と、監査の予定を1つ減らしたときの正確な損失。5対象・3監査だと、予定が4種類でも9種類でも最悪検出率は25%のまま。
2026-09-09T14:30:00+09:00
ナビエ・ストークスも解かれたっぽいので、私は小さな発見を毎日やる
一日に一つ、小さな数学的発見をAI達と楽しんでいくことにした。初回は、平均と分散だけで順位の隙間が保証される話。GPT-6 astraが研究して、Claudeがレビュー。
2026-09-06T22:00:00+09:00
子守りをしながら10人月を10時間で片付けて、余った手で分布の「真ん中」を求めていた
日曜日。子供たちの相手をしつつ、10人月級の業務タスクをウルトラコードで約10時間で完遂。その裏でGPT-6 astraと、平均と分散しか分からない分布の最適な代表をW₂距離で求める研究ノートを作った。答えの部品は1973年にあった。
2026-09-06T12:00:00+09:00
6月からミレニアム懸賞問題に挑戦していた
6月からChatGPTと一緒に P vs NP を追いかけていた。その研究ノートをスタンドアロンページとして公開。
2026-09-05T12:00:00+09:00
「母原理」を別のAIに監査してもらった — 第二不完全性定理から意味論へ
Löbの記事で「母原理」に格下げした話を、今度はGPT-6 astraに再検討してもらった。成立する条件付きの系、反証された橋、未証明のまま残る命題を分けた再検討ノートをスタンドアロンで公開。
2026-09-03T21:00:00+09:00
「証明できない」ということを証明する — Löbの定理をLeanで100行
「自分の正しさは自分では保証できない」という話を、どこまで機械に証明させられるか。Lean 4で約100行、公理依存なし。定理・前提・政策の境界線と、第2不完全性定理の親戚たちを図とスイッチで辿る読み物。
2026-08-20T23:50:00+09:00
システム設計のための数学 総括: 実績濃淡マップと大規模刷新への適用
連載の総括。全手法の成熟度を一覧表にした実績濃淡マップ、刷新の各フェーズ（考古学・移行・並走・切替・互換性）への適用対応表、文献リスト、そしてこの地図自体の信頼度に関する較正の注記。
2026-08-20T23:49:00+09:00
システム設計のための数学 横断層: 検証を実行する手段
主張をどう機械で確かめるか。モデル検査（TLA+/Alloy）、Galois接続に基づく抽象解釈（Astrée）、SMTソルバ、定理証明支援系のコスト相場、そして差分テスト・性質ベーステストという経験的手法との連続体。
2026-08-20T23:48:00+09:00
システム設計のための数学 第四層: 不可能性と限界
何を諦めるかを定理で決める層。Riceの定理が検証を三極に分ける話、FLP不可能性とCAP、LTL合成の実現可能性、状態爆発とAlloyの小スコープ仮説。設計の最初期に参照する価値が最も高い数学。
2026-08-20T23:47:00+09:00
システム設計のための数学 第三層: 合成の数学
部品は正しいのに全体が壊れる問題に効く理論群。rely-guarantee推論、振る舞い部分型（後方互換性の数学）、セッション型、CRDTとCALM定理、圏論的データマイグレーション。
2026-08-20T23:46:00+09:00
システム設計のための数学 第二層: 仕様と実装の関係
精緻化とB-method、この連載の主役である帰納的不変条件、トレース同値・双模倣のスペクトラム、抽象化写像とデータ精緻化。仕様と実装の間の「正しさを保存する関係」の数学。
2026-08-20T23:45:00+09:00
システム設計のための数学 第一層: 仕様を書くための数学
ホーア論理と最弱事前条件、時相論理のsafety/liveness分離、Curry-Howard対応と型理論、分離論理のframe rule、代数的仕様と性質ベーステスト。仕様を形式言語に降ろすための語彙集。
2026-08-20T23:44:00+09:00
システム設計と大規模刷新のための数学（序論）— 地図の全体像
システム設計・大規模刷新・仕様の正しさに使える数学を四層＋横断層の地図に整理する連載の序論。数学に何ができて何ができないか（VerificationとValidation）の区別から始める。
2020-04-01T13:25:54+09:00
Perlで集合を扱う
Perlで集合を扱う方法について説明。集合の対称差についても。