Quaternion Rotations, Claude, and Lean

I got an email message this afternoon reporting a typo in a blog post from about a year ago on converting between quaternions and rotation matrices [1]. The email said exactly where the typo was, but I decided to see whether Claude would find it. Specifically, I prompted Sonnet 4.6 Medium with the following. Write Lean code to verify the two theorems at the top of this post: https://www.johndcook.com/blog/2025/05/07/quaternions-and-rotation-matrices/ That is, prove that the expressions given in the two SVG files are correct. The post included Python code to numerically verify the equations. However, the Python code differed from the LaTeX code for the image in one subscript [2]. Although I asked Claude to prove the expressions in the SVG file produced by the LaTeX code, it detected the conflict between the Python and LaTeX and correctly concluded that the former was correct. The SVG is an image — let me rely on the Python code in the blog (which is the ground truth implementation) and…