Feels like we need a new truth-state for mathematics: "Verified-but-Unproven" for results which we know to be true through formal verification, but without any coherent proof.

I would generally expect this state to resolve quickly to "Proven and Verified" (the tendency in mathematics historically has been for complicated first-proofs of results, followed by significant reductions in proof complexity as new tools and definitions become available), but may still be useful for assigning real credit to who/whatever produces reasonable proof for a brute-force-verified result.