[math-fun] Verification of Musin's proof of 4D kissing number