← Back to context Comment by XCSme 2 months ago > beyond LLMs to specialized approachedDo you mean that in this case, it was not a LLM? 11 comments XCSme Reply D-Machine 2 months ago It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), as clearly described in Tao's posts. Davidzheng 2 months ago Never mind what Aristotle is, verifier llm models are definitely strong enough to verify proofs of elementary methods used here. TeMPOraL 2 months ago Aristotle is an LLM system. D-Machine 2 months 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". 7 replies →
D-Machine 2 months ago It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), as clearly described in Tao's posts. Davidzheng 2 months ago Never mind what Aristotle is, verifier llm models are definitely strong enough to verify proofs of elementary methods used here. TeMPOraL 2 months ago Aristotle is an LLM system. D-Machine 2 months 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". 7 replies →
Davidzheng 2 months ago Never mind what Aristotle is, verifier llm models are definitely strong enough to verify proofs of elementary methods used here.
TeMPOraL 2 months ago Aristotle is an LLM system. D-Machine 2 months 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". 7 replies →
D-Machine 2 months 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". 7 replies →
It could not be done without Aristotle (https://arxiv.org/pdf/2510.01346), as clearly described in Tao's posts.
Never mind what Aristotle is, verifier llm models are definitely strong enough to verify proofs of elementary methods used here.
Aristotle is an LLM system.
"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".
7 replies →