最近の証明支援系／プログラミング言語では、通常の型システムの上位に宇宙システム（ソートシステムともいう）を備えたものがあります。2023年の記事「最近の型理論： 宇宙と世界、そして銀河」の冒頭を引用すると： Lean（最新版はLean 4）は強力な型シス…
古典論理では、命題「Pでない ならば Qでない」の対偶である「Q ならば P」は、もとの命題と同値であり意味は変わらないとされます。しかし、対偶命題がもとの命題と同値なことは日常直感と合わない、とも言われます。そのとき出される実例のひとつに「言わ…
Lean のコード生成に関しては、GitHub Copilot の補完AIやエージェントはほとんど役に立ちません（むしろ、邪魔しやがる）。コーディングAIの利用は現実的でないので諦めました。とはいえ、Lean の複雑な言語仕様や巨大な Mathlib ライブラリを理解・把握で…
2025年内にもう一本ブログ記事を（間に合った）。「生成AIとしゃべる」のは、何かを生成させたいからしゃべるわけです。チャットボットなら会話の応答文を生成させたいし、画像生成AIなら画像を生成させたい、と。目的のモノ、意図したモノを生成させるには…
「AI支援形式証明への道 報告-3 圏論のプラグイン化」への補足記事です。AIに Lean 4 のコードを生成してもらう作業は、通常のプログラミング言語（Python、TypeScript、C++ など）のコード生成とはだいぶ様子が違います。通常のプログラムコード生成に有用…
「AI支援形式証明への道」を書いた頃（2025年11月末）から、AIチャットボットに手伝ってもらって、Lean 4 により定義や定理を記述することを試しています。今のAIは高性能で速いですが、それを使っている僕が低性能で遅いので、全体の進捗は「遅々としている…
「AI支援形式証明への道 報告-1」に書いたように、表〈おもて〉はMarkdown文書だが、裏方・黒子としてLeanファイルを使うコンテンツを考えています。裏方の道具一式がLeanシステム／Lean環境なので、Lean（Lean 4）のインストールが必要です。最近は、VSCode…
昨日の記事「AI支援形式証明への道 報告-1」で、AI支援〈AI-assisted〉の形式記述・形式証明について述べました。強調したい点は、紹介したやり方が off-the-shelf ベースであることです。"off-the-shelf" は、既製品、一般市販品といった意味です。特注品で…
13年前の2017年11月に「ほぼ絶滅 アンミラ」という記事を書きました。 [アンナミラーズで]残っているのは高輪店だけ。懐旧の情だけで品川まで出かける気にはナカナカなれないのですが、高輪店もなくなると、僕はちょっと寂しい気分になりそうです。生き残れ…
「AI支援形式証明への道」は、記述が断片的で分かりにくかったと思うので補足をします。そして、Comet を使って色々試している現状を報告します。内容： Comet について 僕の想定 Comet との経緯 今はこんな感じ オマケ： 絵図証明 関連記事： Perplexity Co…
2023-03-25 のブログ記事「証明支援系がダメだった理由と、AIでブーストする理由」の最後の節を、ちょっと長いですが引用します。 以上に述べたような事情で、5年10年のレンジで見れば、証明ソフトウェアが普及することはないだろうと思っていました。一般の…
AI支援執筆〈AI-assisted writing〉は、誤認・誤解に基づく間違った記述や誤字脱字を（ある程度は）防ぐ効果があります。フェイクニュースや誤情報のフィルタリングが強い（らしい）ので、僕は Perplexity Comet を使っています。Comet は、人間とは比べ物に…
Webブラウザが本来持っている機能以外に何か追加の機能を持たせたいとき、ブラウザ拡張機能（WebExtension）を作ることになるでしょう。しかし、ブラウザ拡張機能を作るのは大変です。ところが、現在のAI付きブラウザなら、自然言語の指示で、けっこうな仕事…
ことの発端は、昨日公開した記事「高次元グラフ上のセルラー層とド・ラーム複体」です。これは長い記事で、誤字脱字や数式の過ちがあるかも知れません。そこで、Edgeブラウザに記事を読ませてブラウザ付属Copilotに校正（誤字脱字の検出など）をやらせようと…
「ニューラル拡散におけるセルラー層と層ラプラシアン」にて： 異種混合ベクトル場に関するド・ラーム複体やホッジ分解を扱うことは興味深い課題です。 これについて少し考えてみました。上記過去記事で述べたセルラー層を高次元に一般化します。高次元とは…
次の論文を斜め読みしました。 [BGCLB23-] Title: Neural Sheaf Diffusion: A Topological Perspective on Heterophily and Oversmoothing in GNNs Authors: Cristian Bodnar, Francesco Di Giovanni, Benjamin Paul Chamberlain, Pietro Liò, Michael M. Br…
「型理論などの引っ越し準備 その2 // 包括自然変換」にて： 「自然変換は関手」で述べたように、アロー圏への関手は自然変換を定義します。包括関手 $`\rho`$ から定義される自然変換を同じ名前で（オーバーロードして）$`\rho`$ とします。 包括関手と包括…
「型理論／論理／インスティチューション理論の引っ越し準備」の続きです。タイトルが長いので少し短くしました。「型理論など」は「型理論／論理／インスティチューション理論」のことです。包括圏の変種（ある種の双対）や包括圏に対する付加的構造につい…
Microsoft Edge 付属の Copilot、「なんでお前に親切に教えてあげないといかんのよ？」と思ってしまうが‥‥ 最後にオベッカ使ってとりなそうとすな。
僕は、ThinkPad がIBM製品だった時代から今まで、ThinkPad をずっと使い続けています。次の写真の下側のノートPCは ThinkPad X1 Carbon Gen 12 で、上に載っている汚れた箱は ThinkPad 701C （バタフライキーボード）の模型の箱です。模型は ThinkPad 10周年…
「ヒルベルトのイプシロン記号のうまい使い方」において、ヒルベルトのイプシロン記号を集合ではなくて集合族に作用させると具合がいい、という話をしました。このことを別な側面から見てみます。$`A`$ が空でない集合のとき、$`\varepsilon\, A`$ は、$`A`$…
普遍性については過去に何度か述べています。 圏論の普遍性が難しい理由 カン拡張の普遍性とは？ 圏論的な普遍構成の代表的な例 前層の表現可能性 再論：指標による記述 「普遍性」という言葉の使い方が無駄に難しいので、出来れば避けたほうがいいだろう、…
“モノイド指標”や“等式を含むモノイド指標”は、デカルト圏のなかの代数構造の定義などによく使われます。必ずしもデカルト圏でなくても、“モノイド指標／等式を含むモノイド指標”は使えます。例えば、圏の自己関手達の関手圏は対称でさえないモノイド圏です…
コアージョン〈coercion〉とは、同じ名前・記号の意味を文脈に応じて変える行為のことです。「どんな文脈ではどんな解釈をするか」という規則はコアージョン規則といいます。ソフトウェアでコアージョンを実装する場合は、コアージョン・グラフというデータ…
エミリー・リエル〈Emily Riehl〉の講義動画の最初のほう（10分くらい）で、ベクトル空間の分配法則の圏論的証明が紹介されています。これは、証明原理としての米田の補題／米田埋め込みとシーケント計算の関連性を示唆していて、なかなか興味深いですね。$`…
表題の「とあるコンマ圏」をちゃんと言うと： 圏 $`\mathcal{C}`$ の米田埋め込み $`よ_\mathcal{C}`$ と、$`\mathcal{C}`$ 上の前層 $`X`$ から作られるコンマ圏 $`(よ_\mathcal{C} \downarrow X)`$ 表題の主張は次の圏同値があることです。$`\quad (よ_\ma…
インデックス付き圏〈indexed category〉の一般化として、インデックス付きn-圏を定義します。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\msc}[1]{\mathscr{#1}} %\newcomman…
過去記事「関手のデカルト射とファイバー付き圏」で次のように述べました。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} `$ 今詳しく説明はしませんが、次の事実は重要です。 圏 $`\cat{C}`$ のアロー圏 $`\mrm{Arr}(\cat{C})`$…
「バンドル-ファミリー対応を簡潔に書く」で導入した簡潔な記法（(-1)乗の書き方）により、随伴トリプルを記述してみます。内容： バンドルの随伴トリプル ファミリーの随伴トリプル バンドルとファミリー バンドルの随伴トリプル次はプルバック四角形です。…
https://x.com/m_hiyama/status/1966421418729763136 にて： (-1)乗の記法はオーバーロードが激しいので「これ以上に用法を増やしたくない」という気持ちはあるのだが：ファイブレーション α のファミリー（あるいはインデキシング）は α^{-1} と書くのが一…
