「AI支援形式証明への道」を書いた頃（2025年11月末）から、AIチャットボットに手伝ってもらって、Lean 4 により定義や定理を記述することを試しています。今のAIは高性能で速いですが、それを使っている僕が低性能で遅いので、全体の進捗は「遅々としている…