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.

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.