この記事は、以前のブログ記事（2025年5月7日掲載）にある四元数と回転行列の変換に関する typo を題材にしています。筆者は、AIアシスタント「Claude」（Sonnet 4.6 Medium）に、その typo を検出させようとしました。具体的には、Claudeに特定のURL（2025年の記事）の冒頭にある2つの定理をLeanコードで証明するよう指示しました。

当初、元記事にはPythonコードによる数値検証と、LaTeXコードによる画像（SVG）の数式表現がありましたが、PythonコードとLaTeXコードの間で subscript に違いがあることが判明しました。Claudeは、この数式の矛盾を検出し、Pythonコードが正しいと結論づけました。筆者は、Pythonコードを「ground truth」として、Lean 4（Mathlib）を用いた検証コードを生成しました。

記事の後半では、生成されたLean 4コードが提示されています。このコードは、四元数から回転行列への変換（Theorem 1）および回転行列から四元数への変換（Theorem 2、Chiaverini–Siciliano）に関する2つの定理を、Leanの公理系を用いて厳密に証明しています。Theorem 1 では、回転行列が直交行列であることを、Theorem 2 では、回転行列の成分と四元数の関係式が成り立つことを証明しています。また、純粋な環の計算によって、四元数の符号に関する恒等式も示されています。

筆者は、 typo の報告に感謝するとともに、数式がLaTeXで記述され、実装がPythonなどで行われる際の不便さにも言及しています。