"Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver"
Not saying it's not an amazing setup, i just don't understand the word "AI" being used like this when it's the setup / system that's brilliant in conjunction with absolute experts.
Eh? The text reads:
"Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver"
Not saying it's not an amazing setup, i just don't understand the word "AI" being used like this when it's the setup / system that's brilliant in conjunction with absolute experts.
That's literally AI though. AI has been around formally since 1956.
https://en.wikipedia.org/wiki/Dartmouth_workshop
AI != AGI != neural networks != LLMs
But Tao did mention ChatGPT so i believe LLMs were involved at least partially.