← Back to context Comment by nextaccountic 1 month ago It was done by a LLM (ChatGPT) 4 comments nextaccountic Reply D-Machine 1 month ago It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links? doormatt 1 month ago And this is Aristotle - https://aristotle.harmonic.fun/It's an LLM. 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". 1 reply →
D-Machine 1 month ago It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), did you even read the links? doormatt 1 month ago And this is Aristotle - https://aristotle.harmonic.fun/It's an LLM. 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". 1 reply →
doormatt 1 month ago And this is Aristotle - https://aristotle.harmonic.fun/It's an LLM. 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". 1 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". 1 reply →
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".
1 reply →