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