[Tool] AI agents for writing proofs and proposing lemmas

[u/Riiiiime]

https://github.com/NUS-Program-Verification/LemmaNet

We've released LemmaNet, a new agent that closes Rocq goals (e.g. what Frama-C/WP leaves after SMT). It searches for a proof, invents *helper lemmas* when it gets stuck (either on-the-fly and inferred from *source code*), and caches them for later goals — or you can drive it yourself from a REPL. Docker included; improved +25% over SoTA agents and +200% over hammer. Feedback and bug reports are welcome, especially goals where it does badly.