There's nothing arcane or particularly theoretical about soundness. It means that if you have an expression of some type, and at runtime the expression evaluates to a value, the value will always be of that type.
For example if you have a Java expression of type MyClass, and it gets evaluated, then it must either throw (so that it doesn't produce any value) or produce a value of type MyClass: either an instance of MyClass, or of one of its subclasses, or null. It will never produce an instance of some other class, or an int, or anything else that isn't a valid value for the type MyClass.
In addition to helping human readers reason about the code, a sound type system is a big deal for a compiler: it makes it possible to compile the code AOT to fast native code, without inserting a bunch of runtime checks and dynamic dispatching to handle the fact that inevitably some of the types (but you don't know which) are wrong.
The compiler implications are what motivated the Dart language's developers to migrate from an unsound to a sound type system a few years ago:
https://dart.dev/language/type-system#the-benefits-of-soundn...
so that they could compile Flutter apps AOT. This didn't require anyone to make their code resemble what you'd do in a theorem prover — it just means that, for example, all casts are checked, so that they throw if the value doesn't turn out to have the type the cast wants to return.
TypeScript is unsound because when you have an expression with a type, that tells you nothing at all for sure about what the value of the expression can be — it might be of that type, or it might be anything else. It's still valuable because you can maintain a codebase where the types are mostly accurate, and that's enough to help a lot in reading and maintaining the code.