rzk-0.5.4: An experimental proof assistant for synthetic ∞-categories