Comment by noddybear
14 hours ago
Nah, its all pattern matching. This is how automated theorem provers like Isabelle are built, applying operations to lemmas/expressions to reach proofs.
14 hours ago
Nah, its all pattern matching. This is how automated theorem provers like Isabelle are built, applying operations to lemmas/expressions to reach proofs.
I'm sure if you pick a sufficiently broad definition of pattern matching your argument is true by definition!
Unfortunately that has nothing to do with the topic of discussions, which is the capabilities of LLMs, which may require a more narrow definition of pattern matching.
Automated theorem provers are also built around backtracking, which is absent in LLMs.