Yes, this is very old. This is a review of Lean 3; Lean 4 is about to appear and this deals with several of the issues flagged by Hales, for example speed.