We’re the #1 formal math model according to ProofBench, by @ValsAI, ahead of the closest competitor by 15%. Aristotle Agent can autonomously prove/formalize for up to 24 hrs without human intervention.

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.