The Computer-aided Discovery of a Theorem about Young Tableaux

Recently a relationship was discovered between the number of permutations of n letters that have no increasing subsequence of length >k, on the one hand, and the number of Young tableaux of n cells whose first row is of length ≤ k, on the other. The proof seemed quite unmotivated and artificial. Here we describe the sequence of events that led to the discovery, via computer algebra, of this relationship.