Once the auto formalization/proving gets much better than this, we will quickly become bottlenecked on knowing/deciding what is the most useful next thing to point it at....which would be quite the exciting and different bottleneck to have and it’s hard to predict what level of productivity that “plateau” looks like. (Assuming that there are also improvements to intelligibility of the proofs themselves, otherwise that too becomes a bottleneck of a similar sort because that’s where a lot of the useful insight lives.)
Yeah my question was a mix of “what’s your next bottleneck” and “what are you/John’s guesses about whether LLMs are fundamentally capable of handling the ‘knowing deciding what to point at’ part, or other stuff that’s more taste-laden.”
Once the auto formalization/proving gets much better than this, we will quickly become bottlenecked on knowing/deciding what is the most useful next thing to point it at....which would be quite the exciting and different bottleneck to have and it’s hard to predict what level of productivity that “plateau” looks like. (Assuming that there are also improvements to intelligibility of the proofs themselves, otherwise that too becomes a bottleneck of a similar sort because that’s where a lot of the useful insight lives.)
Yeah my question was a mix of “what’s your next bottleneck” and “what are you/John’s guesses about whether LLMs are fundamentally capable of handling the ‘knowing deciding what to point at’ part, or other stuff that’s more taste-laden.”