undefined | Better HN

0 pointsdoormatt4mo ago0 comments

And this is Aristotle - https://aristotle.harmonic.fun/

It's an LLM.

0 comments

"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".

nextaccountic4mo ago

Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents

j / k navigate · click thread line to collapse

0 comments

D-Machine4mo 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".

nextaccountic4mo ago

Apparently Aristotle is a LLM with tool calling? Sounds similar to most coding agents

j / k navigate · click thread line to collapse