No it’s not. In fact, much of it is formally verified, which makes it far more reliable than most human-written proofs.

Btw, the most famous human-written proof of the past half-century (Fermat’s Last Theorem) had a massive flaw that took two years and major help from other mathematicians to fix, while the most (in)famous human-written proof of the past 15 years (abc conjecture) is now widely believed to be false.

But people hear what they want to hear I guess.