This is something I’ve been quite excited about for years:

The point at which it’s possible to use LLMs not generate code, but proofs inside a Proof Assistant (like Lean or Rocq), which you then can transform into code and execute.

Because if you treat LLMs as a kind of pretty-well informed, but still fuzzy search over the solution space, a thing that can check the correctness of the output with a very high degree of certainty is excactly what you want. It very much feels like one should be able to have a high iteration speed here.

Let’s see how Theorem turns out.

§ Notes

§ Links

• https://theorem.dev/blog/lf-lean/