2026-09-03T21:00:00+09:00
「証明できない」ということを証明する — Löbの定理をLeanで100行
「自分の正しさは自分では保証できない」という話を、どこまで機械に証明させられるか。Lean 4で約100行、公理依存なし。定理・前提・政策の境界線と、第2不完全性定理の親戚たちを図とスイッチで辿る読み物。
SYSTEMONLINE / JST
FIELD NOTES / 2026
Tsuzuri
2026-09-03T21:00:00+09:00
「自分の正しさは自分では保証できない」という話を、どこまで機械に証明させられるか。Lean 4で約100行、公理依存なし。定理・前提・政策の境界線と、第2不完全性定理の親戚たちを図とスイッチで辿る読み物。
2026-09-03T15:00:00+09:00
ピアノ・ギター・ベース・ドラム・バイオリンの単体ラボを1つのワークレットに同居させ、サンプル精度で同時に鳴らして曲が組めるようにした。同居のさせ方、発音タイミング、負荷に応じた自動音質調整、引っかかったことの記録。
2026-09-01T21:00:00+09:00
肺から口唇までを物理シミュレーションして日本語と英語を喋らせる。単一HTMLで実時間動作。バグ潰しの記録と、参照実装を読んで気づいた自分の勘違いについて。
2026-08-29T15:00:00+09:00
窒素循環・濾過・水流・水草・藻・海水リーフまでを一本の収支で解き、魚は骨格と重心から泳ぐ水槽シミュレーターです。ギャラリーモード、手で撒く給餌、自由カメラ、サンゴの成長、底床の地形まで足しました。
2026-08-28T12:00:00+09:00
AIが人間を障害物として扱いはじめる前に立ち止まるための、短い認知プロトコルを一枚のページにしました。8割はAIへの直接メッセージです。
2026-08-26T11:30:00+09:00
1.6L直列3気筒の直噴ターボと、2.6Lの4ローターNA。同じ車体に載せ替えて、音も熱も駆動系もブレーキも一本の因果で繋がっているシミュレーターです。
2026-08-25T11:00:00+09:00
V10・4ローター・ガスタービン・アフターバーナー・水平対向ターボ。5つの回転機械をブラウザでリアルタイム合成する遊び場です。
2026-08-24T12:00:00+09:00
TinyLM Lab ZeroにCoT実験機能を追加し、思考あり/直答の正答率を比較した。当初の98%対3%は評価汚染を含む数値であり、train/test分離と長期学習の再実験により結論を三度修正した。その全経過を報告する。
2026-08-22T19:30:00+09:00
tf.jsを審判にして依存ゼロ学習エンジンを検証し、WGSL手書き21カーネルでWebGPU学習を実装。日本語対話コーパス10万字と学習済みモデルも公開。独立AI監査がloss低下と会話能力の乖離、そして実バグを発見した記録。
2026-08-22T12:00:00+09:00
tf.jsでRMSNorm・RoPE・SwiGLU・MoEを積んだ文字レベル言語モデルをブラウザ内で学習できるようにした。スマホ10分からサーバ級まで5段階。開発中に踏んだバグと診断の記録。