You were misrepresenting what actually happened b/c you want to believe in magic. I'm not calling it magic, I'm saying your interpretation of events is magical b/c you don't actually understand how computers work. There is nothing magical about theorem proving, Isabelle/HOL has been doing it for decades.

Isabelle/HOL haven't been solving open problems, as far as I'm aware. They've been used for making fully-formal proofs of problems that were already considered proved to a satisfactory level by the mathematical community. I believe mathematicians generally consider proving something to the mathematical community the "hard part", while making it fully formal is just a kind of tedious bookkeeping thing.