I was studying Erdos problems by only taking ChatGPT 5.5 outputs and just asking it to keep on attempting to solve it by asking it to go further. I haven't started doing this with chatgpt 5.6 I have some partial results here https://chatgpt.com/g/g-p-69f03400f420819192418b18ca90ffee-d...

What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to be published.

While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/

I haven't played around with Aristotle at all, thanks for bringing it up & (also your codebase, thesisus, is very solid!)