I guess I don't understand the issue you're raising. If you want to formalize a non-constructive proof, it remains non-constructive, even if you have a computer check the proof vs a human.

As a trivial example, in lean you can work with probability theory/measure theory. This has oodles of non-constructive parts, but we can ignore that for now. As part of this, you can use the probabilistic method. For example, if you want to prove that codes with optimal parameters exist, for many noise models it is known that sampling a code randomly from an appropriate (and often naive) distribution will yield a code with optimal parameters.

You should be able to prove this in lean (or any other theorem prover). But you cannot construct these codes. While you can sample a code randomly, verifying a code has good parameters is typically NP-hard (e.g. it is an instance of the minimum distance problem). So, you cannot (efficiently) "construct" a good code in lean4, despite being able to prove one exists.

This seems analogous to me that you could validate that a non-constructive proof is correct in lean4. Sure, it would be nice if the proof was constructive. But it isn't, and encoding it into a computer shouldn't give you that (non-trivial) property for free.