alt Hacker News> 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?
> 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?
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.