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.

[Tarun22r]

Aristotle is designed to automate high‑level math problem solving by mixing natural language reasoning with formal verification tools. It’s especially aimed at tough problems (like those at the International Mathematical Olympiad level) where both creativity and strict correctness are needed.