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