Things constructivist mathematics cannot do: 1) Prove Addition of natural numbers. 2) Prove two real numbers are equal. RNNs are only TC with infinite precis

Things constructivist mathematics cannot do: 1) Prove Addition of natural numbers. 2) Prove two real numbers are equal. RNNs are only TC with infinite precision and unlimited resources, once you have finite precision they are very limited. LLMs do not have recursion at all and can't even emulate finite automations. In fact soft attention can only emulate TC_0 Feed forward networks are effectively DAGs and with soft attention, DAGs built with AND,OR, NOT, and threshold circuits. One of the state of the art inference in code methods is bi-abduction, probably best described here. https://fbinfer.com/docs/separation-logic-and-bi-abduction/ https://fbinfer.com/docs/separation-logic-and-bi-abduction/ But this localization makes it computationally possible, and has limits. The qualification and frame problems, combined with the very limited computational power of transformers is another lens. LLMs being formalized doesn't solve the problem. Fine tuning and RAG can help with domain specificity, but hallucinations are a fundamental feature of LLMs, not a bug. Either a use case accepts the LLM failure mode (competent, confident, and inevitably wrong) or another model must be found. Gödel showed us the limits of formalization, unless we find he was wrong, that won't change.