[D-Machine]

"Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver"

It is far more than an LLM, and math != "language".

[nextaccountic]

Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents