[zitterbewegung]

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/

[colin7snyder]

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

[universa1]

This looks interesting. I am not really familiar with lean, etc... Could I use this to formalize/verify a proof from a paper?

[zitterbewegung]

With Aristotle you could formalize a proof from only the text of a paper.

[trenchgun]

Yes, assuming the stuff it depends on is already formalized.