sdenton4
4 hours ago
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.
bemtevi
6 minutes ago
> 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),
A bit of an oversimplification, I think. Definitely there are some simplifications, but I wouldn't say really significant to the point where "resolve quickly" follows, along the lines of what you said.
Most complicated math is still nearly as complicated as when it was invented. Simplifications to presentation maybe, and some reduction in the proof difficulty yes, but not to the point of being significant in the way you describe. Any modern result that has been around for 20 years likely hasn't undergone a serious simplification, for example.
cadamsdotcom
3 hours ago
Sounds like a 2x2 matrix.