Comment by D-Machine
2 days ago
It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links?
2 days ago
It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links?
And this is Aristotle - https://aristotle.harmonic.fun/
It's an LLM.
"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