If I understand correctly, the "fastest program f" is the one which M not only proves to solve the problem, but also proves to solve more quickly than any other provable time bound.  That is, it's not so much "fastest program f" as "program f with the lowest provable time bound among programs with provable time bounds relative to the proof system".  This is another critical constraint that I should have mentioned earlier - the result really is a lot weaker than the abstract makes it sound.