It was done by a LLM (ChatGPT)

D-Machine · 2026-01-09T23:45:18 1768002318

It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links?

doormatt · 2026-01-09T23:58:24 1768003104

And this is Aristotle - https://aristotle.harmonic.fun/

It's an LLM.

D-Machine · 2026-01-09T23:59:34 1768003174

"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 · 2026-01-10T05:51:23 1768024283

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