It is unlikely that such proof can be considered a contribution to mathematics. Finding "elegant" proofs (and not just "facts"), building conceptual frameworks in the process, is the heart of mathematics as a human activity.
This isn't really true. Many proofs often start as dozens or hundreds of pages long, yet the creator is credited with advancing mathematics. It isn't till later that someone else comes along and simplifies the proof.
Haha this is the first thing I've heard about mathematics that reminds me of statements I've heard about chess. It's interesting to imagine a future in which useful math supporting useful tech is done by brutish AIs, while elegant math is the last refuge of humanity.
But the thing which constructs the proof might be what we will consider to be an "elegant proof." It might be more unsatisfying not being able to understand exactly why something is true, but computers can greatly expand the reach of what we can know.
>It is unlikely that such proof can be considered a contribution to mathematics. Finding "elegant" proofs (and not just "facts"), building conceptual frameworks in the process, is the heart of mathematics as a human activity.
Not really. All kinds of non-elegant, 80 and 200 page proofs (a proof doesn't have to be brute force to be inelegant) are regularly churned and appreciated every day.
Those are in fact the bread and butter of mathematics in practice, not the few and far between elegant proofs people read about.
Can't these proofs be useful in the context of "given that X is true we can say that"? In that case it doesn't matter how X was proven, it just provides a tool for future mathematics.
Ultimately, in mathematics it is important to understand why something is true; simply knowing that someone (or something) "says so" is never good enough.
