Quaternion Rotations, Claude, and Lean

This article describes an experiment where the author used Claude (Sonnet 4.6 Medium) to generate Lean 4 code to formally verify two theorems about converting between quaternions and rotation matrices. The process involved detecting a typo in the blog post's alt text, relying on Python code as the ground truth, and iterating with Claude to produce correct Lean proofs. The article covers quaternion algebra, rotation matrix properties, orthogonal matrix verification, and the Chiaverini–Siciliano method for extracting quaternions from a rotation matrix, demonstrating AI-assisted formal verification in mathematics.