[sdeframond]

> Would we regard that as a major achievement of the mathematician? I don’t think we would.

1. Does it matter, really? 2. Is it very different from previous computer-aided proofs, philosophically?

[agnishom]

1. It matters because there are human mathematicians who pride themselves for their mathematical achievements. Mathematics is art to them.

2. Yes, it is. Because pre-LLM era computer-aided proofs were about using the computer to either solve a large number of cases or to check that each step in a proof mechanically follows from the axioms.

[snoman]

1. And some that are equally skilled that don’t. It matters, internally, to them but it needn’t matter to anyone else.

[agnishom]

On the flip side, there are people (like me) far less skilled that do (take joy in the appreciation of mathematics as art).

[layer8]

It matters because most mathematicians thrive on the recognition of their achievements. If what you do any mediocre mathematician could have done, that takes away motivation and fulfillment.