Deepseek r1 is getting a lot of buzz in the last day or so. As a Chat agent in Cursor, it gets further than I've seen other AI get at writing Lean 4 code.

The process is acutely painful. It can't stick to directions, and keeps trying to add proof features that it can't get to work, despite my instructions that we're using Lean 4 as a general purpose programming language.

To my surprise, the code ran faster than either Haskell or Rust on a small case. There could be so many artifacts involved in such a conclusion, but larger cases blew the stack. That's just inexperienced code.