This is a principle I've been thinking about recently that we should discuss. The problem is that improvements in automation can break existing proofs. As the system grows, this is an increasing challenge -- potentially O(n^2) where n denotes the size of the system because every time you improve the automation, you could potentially break a significant fraction of the proofs. In practice it shouldn't be nearly this bad because, as the system develops in different direction, only a small fraction of the system has the potential to "break" a large fraction. That is, some theories are more fundamental than others. Furthermore, the more fundamental theories will tend to be developed more. As the automation features of those fundamental theories improve, they should asymptote to an "optimal" limit. We can never expect to be fully "optimal" since we can always expect there to be more clever ways to do this, but we can start to standardize expectations for the best automation we can provide. As we approach those standards, those theories become more stable (in the same sense that the slope of a smooth function decreases as you approach a maximum).
This is a principle I've been thinking about recently that we should discuss. The problem is that improvements in automation can break existing proofs. As the system grows, this is an increasing challenge -- potentially O(n^2) where n denotes the size of the system because every time you improve the automation, you could potentially break a significant fraction of the proofs. In practice it shouldn't be nearly this bad because, as the system develops in different direction, only a small fraction of the system has the potential to "break" a large fraction. That is, some theories are more fundamental than others. Furthermore, the more fundamental theories will tend to be developed more. As the automation features of those fundamental theories improve, they should asymptote to an "optimal" limit. We can never expect to be fully "optimal" since we can always expect there to be more clever ways to do this, but we can start to standardize expectations for the best automation we can provide. As we approach those standards, those theories become more stable (in the same sense that the slope of a smooth function decreases as you approach a maximum).