Post

1/4 Here is a video of neuro-symbolic theorem proving in action using the (opensource) Rocq-piler MCP (we renamed when updating to Rocq) with the Rocq theorem prover.

gavin.codes

@gavin.codes

2/4 We (at Scidonia) have spent considerable effort to increase the theorem proving ergonomics for LLMs with our MCP and have gotten the following one-shot for a type preservation theorem about the programming language PCF with references (sort of a micro-ML language) on video.

30/5/26, 1:11 pm0 reposts0 likes

gavin.codes

@gavin.codes

30 May

3/4 Model: DeepSeek v4 Tokens to completion: 141k Cost: $3.43 Time: 20m (video is at 10x speed)

gavin.codes

@gavin.codes

30 May

4/4 You can get Rocq-piler here: github.com/scidonia/roc...

github.comGitHub - scidonia/rocq-piler: MCP server for Coq LSPMCP server for Coq LSP. Contribute to scidonia/rocq-piler development by creating an account on GitHub.