Well, they of course not defy computer science. The "trick" is that they are not Turing-complete, they mandate termination of every expression.

Also, most of them are made to prove stuff first and foremost and thus trade off a lot of performance to the point that it makes them practically unusable for many stuff (e.g. numbers may be represented as an object that has n-1 further children recursively), though Lean is an exception as you note.