| ▲ | doormatt a day ago | |||||||
And this is Aristotle - https://aristotle.harmonic.fun/ It's an LLM. | ||||||||
| ▲ | D-Machine a day ago | parent [-] | |||||||
"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". | ||||||||
| ||||||||