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…