There is a very active community around Lean ranging from mathematicians with no clue about computers to AI researchers trying to improve the automation. These AI researchers have explicitly said that bigger training sets will be very helpful. But like the sibling comment says, AI is not the main point.