You can probably train a language model to lead mathematicians on a wild goose chase for quite a while, by just proposing some definitions, proving a few trivia

You can probably train a language model to lead mathematicians on a wild goose chase for quite a while, by just proposing some definitions, proving a few trivial things about it, proposing another based on that and doing the same etc. Then you can see how long it takes for them to catch on that it's not actually going anywhere. It seems to me older math texts in particular expect a lot of trust that there's some light at the end of the definitions tunnel. It's become more acceptable to talk (in human language) about motivations, of why we choose to go one particular path in the space of all possible constructions. And that's the clue with math AIs too, isn't it? I'm sure they can prove endless things, but will it be things anyone cares about, unless they have carefully human-supplied motivations?