HOL is a classical (i.e. non-constructive) logic based on simple type theory, and that makes proof automation much easier. Adapting the kind of proof automation that classical logic with simple types enables to a Curry-Howard based prover with dependent types (like Lean, Coq or Adga) is not a fully solved problem.
For industrial-scale program verification, proof automation is everything! Nothing else matters.
I conjecture, but don't know, that Amazon write their HOL-based prover from scratch, to take into account their cloud resources. So it might well be the most modern prover of all.
Note that Leonardo de Moura, who initiated Lean, is now at AWS. To add even more complications, AWS does also use Lean, e.g. https://github.com/leanprover/SampCert
I don't know, but given that AWS has 1000s if note millions of servers that may have idle cycles, it makes sense to use them for automatic theorem proving. And there is no existing ITP or even SMT solver that was specifically designed for efficient use of so much parallelism.
AWS certainly hired a lot of senior STM and ITP guys, such as John Harrison.
At 1:27, "So then, you can ask, why didn't [Apple and AWS] choose Coq, Lean or Agda [instead of Isabelle/HOL]?"
My understanding (having only used dependent-types -family interactive theorem provers) is that if your property can be expressed in HOL, proving it will require far less human effort to prove than Coq or similar.
There ist Jeremy Avigad's influence. He is not the typical type theorist and definitely no constructive zealot.
"I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation.."
"Many parts of classical mathematics, however, have not been developed
constructively."
Related response [0] and [1]. It is a bit of a matter of taste: I prefer classic stuff as I have used that for decades. HOL is ‘easy’, but I haven’t spent as much time with Lean.
