During the live debate Tsvi linked to, TJ (an attendee of the event) referred to the modern LLM paradigm providing a way to take the deductive closure of human knowledge: LLMs can memorize all of existing human knowledge, and can leverage chain-of-thought reasoning to combine that knowledge iteratively, making new conclusions. RLVF might hit limits, here, but more innovative techniques might push past those limits to achieve something like the “deductive closure of human knowledge”: all conclusions which can be inferred by some combination of existing knowledge.
This “deductive closure” concept feels way too powerful to me. This is even hinted at later in the conversation talking about mathematical proofs, but I don’t think it’s taken to its full conclusion: such a deductive closure would contain all provable mathematical statements, which I am skeptical even an ASI could achieve.[1]
To spell this out more precisely: the deductive closure of just “the set theory axioms” would be “all of mathematics”, including (dis)proofs for all our currently unproven conjectures[2] (e.g. P ≠ NP), and all possible mathematical statements.[2]
Well, as long as we want to stick to some reasonable algorithmic complexity. Otherwise the “just try all possible proofs in sequence” algorithm is something we already have and works perfectly.
This “deductive closure” concept feels way too powerful to me. This is even hinted at later in the conversation talking about mathematical proofs, but I don’t think it’s taken to its full conclusion: such a deductive closure would contain all provable mathematical statements, which I am skeptical even an ASI could achieve.[1]
To spell this out more precisely: the deductive closure of just “the set theory axioms” would be “all of mathematics”, including (dis)proofs for all our currently unproven conjectures[2] (e.g. P ≠ NP), and all possible mathematical statements.[2]
Well, as long as we want to stick to some reasonable algorithmic complexity. Otherwise the “just try all possible proofs in sequence” algorithm is something we already have and works perfectly.
Well, as long as they are not undecidable.
You’re right. I should have put computational bounds on this ‘closure’.