# @davidad — 2024-09-14

♥28 ↻1 · https://x.com/davidad/status/1834919718576123917

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 &amp; proof assistants” to make future GPTs useful. https://t.co/8RRhMILSSd

tags: author:davidad, kind:tweet, model:o1, on:o1, year:2024
cited on: _dossiers/o1.md, o1
