But what does it mean? The theorems are just symbols in lean. The conjectures humans chose are carefully selected to be the questions that are interesting and relevant to our intuition about the real world.

Math often doesn't have applications for hundreds of years and that application is only possible because people deeply understand it and how it applies to the real world.

Generating an endless list of true statements doesn't really do anything, those things are already true regardless of whether someone has written a lean program to model them.