The reasoning that earned IMO gold, applied to formal verification of software, hardware, and mathematics. Every output backed by a machine-checked proof.

Give it an English problem and it will prove and formalize from scratch, or it can work and edit files directly inside your Lean project or code repository.

Leaders of large-scale formalization projects are increasingly accepting Aristotle's code contributions with no modifications.