Can someone help to understand how Aristotle model works?

[nnarek]

Aristotle model from Harmonic currently one of best models in formal verification. It seems like they are using Claude(or finetuned open source model) and tools to interact with Lean4. I will be very glad if someone can find out which model they are using and some architectural details

[jconnorlaw-ai]

See it's architecture in the team's flagship paper, Aristotle: IMO-level Automated Theorem Proving.