I actually somewhat sympathize with your view. But I think you overstate the problem: if someone discovers something with Mathematica, they can then formalize it with an open proof assistant like Coq before they publish, and modern journals in fact encourage this sort of thing.
Really, it's not a zero-sum-game between open-source and commercial tools.
Really, it's not a zero-sum-game between open-source and commercial tools.