@tao

Thanks for sharing this. I think the workflow with Claude Code can be very different and much less hands-on than you approach it in the video.

I have recently taken an old paper of mine and tried to let claude code formalize it with only very minimal intervention.

After two weeks one not entirely trivial Gröbner basis proof (Theorem 1.1) is done. Currently it is working on a primary decomposition statement:

https://github.com/tom111/BEI-lean

Will share more details in a forthcoming blog post.