Comment by 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.
2 days ago
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".
> Aristotle integrates three main components (...)
The second one being backed by a model.
> It is far more than an LLM
It's an LLM with a bunch of tools around it, and a slightly different runtime that ChatGPT. It's "only" that, but people - even here, of all places - keep underestimating just how much power there is in that.
> math != "language".
How so?
6 replies →