Sequent

A big part of that acceleration comes from early access to @Sequent_Inc's Alan, a state-of-the-art AI-powered prover agent which performs autonomous proving and also assists with specification modeling and theorem generation

Lean is fashionable in math right now, but as @LawrPaulson argues, other frameworks have their own advantages. HOL4 was built for applications beyond math (hardware, software, compilers) and that's why we use it!