How can humans discover proof plans?
This is an art similar to the skill used by a good mathematics teacher when analysing a student’s proof or explaining a new method of proof to a class. The key is identifying the appropriate meta-level concepts to generalise from particular examples. Armed with the right concepts, standard inductive learning techniques can form the right generalisation (see the answer about learning new proof plans for more information).