Property-based testing is not proof-based, but stochastic; you define the input space for a property fairly well, then the testing framework samples random points within that space. They also generally have reducers, which try to create small failing inputs iteratively after finding one failing input. The difference with fuzzing is mostly that fuzzers are largely black box; the input space is left largely undefined (e.g. AFL: bag of bytes), and the property under test is usually "well, uh, does it explode?". I don't think the popular property-based testing frameworks use instrumentation to guide exploration of the input space.

It is and isn't.

The type system will try to prove that a program will behave in some specific ways without needing to run the program. The "specific ways it behaves" is what I call "properties".

Property based testing will run the program and check as it is running that it behaves in some specific ways.

In the end, they both can be used to demonstrate that some properties of a program execution hold, but they go about it differently.

The type system will use logic over the code semantics and structure to assert that in all possible cases (combination of inputs) the property will hold.

The property based testing will use sampling to assert that in a lot of cases (combination of inputs), the property will hold.

Unless you can sample the entire input range in a property based test, you don't prove that it holds for all inputs, just for a large number of them. While type systems tend to prove for all inputs.

Also generally the type system will take less time to execute its reasoning over the code, than the property based test will take to run its sample set.