> Automatically discovering formal (i.e., unambiguous) solutions to novel problems can never be automated.

Things like alphafold would suggest to me that this doesn’t always hold true.

Perhaps a matter of definition but to me there does seem to be “some” problem solving ability. And once you’ve got even a little of that then it’s a scaling question and not really compatible with “ can never be automated.”