Tao assesses o1’s helpfulness with new research as “a mediocre, but not completely incompetent, graduate student.”Tao finds Lean 4 useful—but not yet GPT.He suggests “integration with other tools, such as computer algebra packages & proof assistants” to make future GPTs useful. https://t.co/8RRhMILSSd
cited on: o1
Reproduced against link rot, credited and linked to its original. Yours and you’d rather it weren’t here? Open an issue.