Type theory lets you specify natural language as a computer program, and determine equivalence of proofs as a computational sequence of symbols. It's pretty weird, but also cool. It's why we have the ability to computationally generate mathematical theorems without understanding them.
And since LLMs are also just symbol manipulators, it's partly why LLMs can make mathematical proofs without understanding of the underyling math.
It also calls into question whether we are just automaton symbol manipulators, who just happen to give some sequences of symbols special meaning
I’m sure what you’re saying is very interesting, but I’m only just getting a grasp at its meaning
maybe because my last college class was almost, nearly a decade ago
30s are a different ball game innit?
Great take! But as a musician from Nigeria, this is where art breaks the theory.
A computer can generate a theorem without understanding it, and an LLM can generate a proof. But a computer cannot feel why a minor chord makes us sad.
We don't just give sequences special meaning — we give them soul. Type theory explains the HOW of symbols, not the WHY we cry when we hear them.
Maybe we are symbol manipulators, but we are the only ones who manipulate symbols to worship, to love, to protest. That choice IS the meaning.