Inputs:axis is k=(0,0,1), the unit z axis; angle is θ=1.5708≈π/2 radians.
Skew matrix: with kx=ky=0 and kz=1, [k]× has rows (0,−1,0), (1,0,0), (0,0,0). Its square is diagonal with entries (−1,−1,0).
Coefficients:sinθ≈1 and cosθ≈−3.67×10−6, so 1−cosθ≈1.
Sum:I+[k]×+[k]×2. The diagonal becomes 1−1=0, 1−1=0 and 1+0=1; the skew part adds −1 at row 1, column 2 and +1 at row 2, column 1, giving [[0.0, -1.0, 0.0], [1.0, 0.0, 0.0], [0.0, 0.0, 1.0]].
Output: a 3×3 nested list of floats, shown rounded; the raw diagonal is really cosθ≈−3.67×10−6 since 1.5708 is not exactly π/2.
Notice the first column (0,1,0): the x axis lands on the y axis (counterclockwise 90°), while the z column is untouched: points on the axis never move.
Axis–angle is a minimal 3-parameter representation of 3D rotations: a unit vector (rotation axis) and a scalar angle, while a rotation matrix is a 3×3 orthonormal matrix in SO(3). Rodrigues’ formula gives a direct, smooth mapping from axis–angle to a rotation matrix using sines and cosines of the rotation angle and a skew-symmetric matrix built from the axis. This is heavily used in SfM/SLAM because it is both numerically stable and easy to differentiate for optimization.
In practice, you often store a rotation as a 3D vector \mathbf{r}∈R3, where its direction is the rotation axis and its magnitude is the rotation angle: \theta=∥\mathbf{r}∥,\mathbf{k}=\mathbf{r}/\theta. Rodrigues’ formula then produces a 3×3 matrix R that you can use to rotate 3D points, compose poses, and compute Jacobians with respect to the three parameters.
1. Background Knowledge (concepts/theory)
SO(3) and rotation matrices
3D rotations form a Lie group called SO(3): the set of 3×3 real matrices R such that R⊤R=I and det(R)=1.
Rotation matrices are redundant (9 entries with 6 constraints) and can be awkward in optimization.
Axis–angle and the Lie algebra so(3)
Any 3D rotation can be represented by a unit axis k and an angle θ.
The Lie algebra so(3) is the space of skew-symmetric3×3 matrices; each such matrix corresponds to a 3D vector via the hat operator: