I'm extremely sad that, in all of this, it is hard to celebrate the use of formal verification as a tool for genuine progress in the mathematical frontier... the LLMs that enable it are too entangled with commercialization.