Category error! I'm sick to the back teeth of wrongheaded comparisons of inanimate objects to humans. It's so rife even colleagues do it. What's next?
> I compared a rock and a person, and challenged them to stay still the longest and the rock won! Wow!
Things thought up by the unhinged & those who wish to dehumanise for profit.
@olivia @abucci @Iris How do I put this? I find the "category error" criticism accurate. And it rightly prepares and leads into the socioeconomic criticism of dehumanisation of work and into the sociopsychological deskilling criticism.
What I wonder is: is there any "progress" or "benefit", say, of/for the discipline of mathematics once a certain proof exists (assuming the rest of the discipline manages to continue evolving without deskilling) that we risk blinding ourselves to by just insisting that AI isn't itself "proving" things? This focus on the category error makes it sound like if we managed to avoid anthropomorphisation and use different vocabulary for the function AI plays, the criticism would miss the point.
1/2
While writing this, it occurs to me that it's naïve to assume what is in brackets above: that the disipline can evolve in an "untainted" way while accepting on a regular basis proofs that have not been conceived by human scholars. But what kind of taint is that? - I have a hunch it's none of the problems mentioned before. Or is it?
I'll re-read your nice paper on "human-centered AI" and think about how its analyses apply to maths as a discipline.
2/2
Hi Anthony, thanks for your response.
The scenario I had in mind was mathematicians of the 2070s still being pretty much like our mathematicians today and those of the past, and looking at the corpus of problems, theorems and proofs established until then, and not caring much about when and in which way a specific proof was introduced. As long as the proof itself is correct as evaluated by those mathematicians themselves. Proving and correctness may lie in the eyes of the human observer, not in the neural network that has outputted the proof. But that does not detract from said correctness at all. I feel uneasy if we focus mainly on how we call this "outputting" or deny that there is a new proof there.
I have already ack'd in the other toot: the scenario is naïve insofar as it assumes the only thing to have changed would be a handful of additional proofs with a different genesis. I'd like to understand the other changes we should expect for the discipline.
@anwagnerdreas @abucci @olivia @Iris
I see it as twofold: a burden of proof argument, and a question about where energies are best spent. For the former, whenever proposing a new tool, the onus is on the person advancing said new proposal to show that it works, or at least works well enough to be worth consideration.
For the second, cranks *could* be right about their wild mathematical claims, but we rightly often reject them out of hand as a timesaving heuristic.
@anwagnerdreas @abucci @olivia @Iris It's impractical to individually evaluate the claims of every crank theorem, and so we largely don't do it.
When it comes to LLM-generated "proofs," I think it's worth comparing to Lean and other formalized proof systems. We rationally have enough confidence in how Lean builds proofs from lower-level theorems and axioms that it's worth approaching Lean-based proofs in good faith. LLMs, by contrast, do not offer any such structure we can use.
Olivia Guest · Ολίβια Γκεστ
Anthony
Andreas Wagner
Cassandra is only carbon now
Eric Lawton
Fazal Majid