DeepSeek-Prover-V2

I am a computer science researcher interested in evaluating the use of LLM in theorem proving. There is a specialised model from DeepSeek that is specifically designed for that purpose. I would love to see it added to Cursor.

it will never happen as cursor integrates general models(as of now), you got two options:

  1. install openrouter mcp and prompt a cursor model to use this mcp tool in order to process your request through model “deepseek-prover-v2”
  2. directly use openrouter by configuring it in cursor settings and adding deepseek-prover-v2 as a custom model in the list of models like Dean explains here: Connecting Poe.com API with Cursor to access ChatGPT - #6 by deanrie

If you need agentic capabilities go with 1

1 Like

Thanks! I am interested in trying agentic capabilities, so option 1 seems to be a way to go. Where I can find more info on option 1? Ideally step-by-step instruction?

Sure, here Cursor – Model Context Protocol it guides through installing and usage, here’s my config for openrouter:

"openrouter": {
  "command": "env",
  "args": [
    "OPENROUTER_API_KEY=your-api-key-goes-here",
    "npx",
    "-y",
    "@mcpservers/openrouterai"
  ]
}

Then choose your cursor preferred model(o3 is best in benchmarks for math and reasoning) and ask it to:

  • process this prompt through openrouter mcp tool with model “deepseek-prover-v2”: …your prompt for deepseek
  • analyze the result […]
2 Likes