I have fixed the target data structures and also make Claude compare the generated code against a python reference via PBT. However, the vibe-coded code generator stumbles upon a missed clone/copy case every now and then. This is where I am less certain that it converges.

> I run into bugs all the time so it’s probably not ready for anyone other than me to use, but I’ve managed to go pretty deep (if not wide) in just a few days of work.

Having similar experience with my experimental code generator to Rust. Every time a yet another example does not work, Claude fixes it. However, I am curious whether it would converge to a bullet-proof solution, or I have to carefully read the code and come up with proper abstractions.

Litex is probably closer to TLA+ than to Lean. Both draw inspiration from untyped set theory and LaTeX.

> Just friendly remember that Open access publishing is the new business model that is more lucrative for publishing industry and it is basically a tax on research activities but paid to private entities and mostly paid by taxpayer money...

While I do not disagree with this statement, this makes a significant difference for the citizens who do not happen to work in academia. Before open access, the journals would try to charge me $30-50 per article, which is ridiculous, it's a price of a textbook. Since my taxes fund public research in any case, I would prefer to be able to read the papers.

I would also love to be able to watch the talks at academic conferences, which are, to very large extent, paid by the authors, too.

It probably will, but not the way we all imagine. What we see now is an attempt to recycle the interactive provers that took decades to develop. Writing code, experimenting with new ideas and getting feedback has always been a very slow process in academia. Getting accepted at a top peer-reviewed conference takes months and even years. The essential knowledge is hidden inside big corps that only promote their "products" and rarely give the knowledge back.

LLMs enable code bootstrapping and experimentation faster not only for the vibe coders, but also for the researchers, many of them are not really good coders, btw. It may well be that we will see new wild verification tools soon that come as a result of quick iteration with LLMs.

For example, I recently wrote an experimental distributed bug finder for TLA+ with Claude in about three weeks. A couple of years ago that effort would require three months and a team of three people.