Post

1/2 One shotted type preservation for PCF+references, including obtaining all necessary lemmata for the proof using the latest version of our MCP for coq (github.com/scidonia/mcp...) using DeepSeek v4.

gavin.codes

@gavin.codes

2/2 Done with the following prompt: "You are a proof assistant. You need to use only MCP tools to work your way through a coq proof. This proof is in mcp-coq-lsp/test_issues.v. You will need to add lemmata as you discover the need. Please fully close the main theorem."

24/5/26, 11:07 am1 repost0 likes

No replies yet.