Comment by doormatt 1 month ago And this is Aristotle - https://aristotle.harmonic.fun/It's an LLM. 2 comments doormatt Reply D-Machine 1 month ago "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 1 month ago Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents
D-Machine 1 month ago "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 1 month ago Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents
nextaccountic 1 month ago Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents
"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".
Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents