For now, I’m not very familiar with server rentals myself. However, the requirements can change quite a bit depending on how much quantization you are willing to accept and which inference backend you plan to use:
There do seem to be a few realistic routes. I do not have a personal server contact to introduce, but the public options currently fall into three useful categories:
| Goal |
A reasonable starting route |
Main caveat |
| Try the model on a few problems |
A serverless API or managed deployment |
The provider’s weight conversion, revision, sampling implementation, or quantization may differ from the released checkpoint |
| Self-host the released checkpoint with relatively little compromise |
A single 8×H200 SXM/NVLink node is the first configuration I would investigate |
I have not found a complete, reproducible public deployment report for this exact Prover-V2 checkpoint |
| Use an available 8×H100 node |
A quantized/converted checkpoint, or possibly offloading |
This is a different experimental condition from serving the released weights directly |
| Reproduce paper-level pass@k results |
Self-hosted deployment plus a pinned Lean/evaluation environment |
Loading the model is only one part of the experiment |
My default route would therefore be:
- Use a managed endpoint for a small smoke test, unless exact self-hosting is already a hard requirement.
- If the released weights must be self-hosted, look first for a single physical 8×H200 SXM node with NVLink/NVSwitch, sufficient local storage, and a known-good vLLM or SGLang container.
- Only commit to a longer reservation after a short validation run that includes actual Lean compilation—not just successful text generation.
The main reason I would not treat all of the listed GPU configurations as interchangeable is memory. The Hugging Face repository currently shows about 689 GB of files, while 8×H100 80 GB provides 640 GB of raw GPU memory before accounting for runtime allocations. Repository size is not exactly the same as runtime memory consumption, but it is a strong warning against assuming that the released checkpoint is a straightforward 8×H100 deployment.
For the closely related DeepSeek-V3/R1 architecture, NVIDIA’s TensorRT-LLM DeepSeek guide states that FP8 weights require about 671 GB by themselves, with additional memory needed for activations and KV cache. Its framework-specific minimum table lists:
- 16×H100 80 GB for FP8
- 8×H200 for FP8
- 8×B200/GB200 for FP8
- 8×H100 for W4A8
This is not a direct guarantee for DeepSeek-Prover-V2, but it is a useful same-family reference because the official Prover-V2 model card says that the 671B model shares the DeepSeek-V3 architecture.
There is also an official vLLM example for serving DeepSeek-V3-0324 on a single 8×H200 node using data parallelism and expert parallelism. That makes 8×H200 look like a technically plausible starting point, although it is still not an exact Prover-V2 deployment report: vLLM Expert Parallel Deployment.
Public routes that seem worth checking
These are examples rather than endorsements, and availability can change.
Managed access
These could be useful for checking prompts, output extraction, generation length, and Lean verification before renting a complete node. I would not assume that either service is bit-for-bit equivalent to the released HF checkpoint without asking about the exact model revision and conversion process.
Raw 8×H200-style nodes
The useful part of these examples is not merely the provider name. It is the target specification: eight H200 SXM GPUs in one physical server, connected through NVLink/NVSwitch, rather than eight separately allocated GPUs.
Before reserving anything, I would prefer a provider that can offer:
- a short validation window;
- the GPUs in one physical node;
- persistent local storage or a pre-cached checkpoint;
- a pinned, known-good serving container;
- SSH or sufficient container control for the intended workflow;
- confirmation of the exact GPU topology.
A minimal provider description such as “8×H200 available” is not quite enough for this model family.
Why 8×H100, 8×H200, and 16×H100 are different cases
1. The released checkpoint and 8×H100
The HF repository currently reports approximately 689 GB of files and identifies the tensors as a mixture of BF16, FP8, and F32. Eight 80 GB H100s provide 640 GB of aggregate physical VRAM.
The repository size is not a perfect calculation of the amount allocated by a particular runtime. For example, an engine may transform, repack, shard, or offload weights. Nevertheless, it suggests that the released checkpoint is not a simple “download it and use tensor parallelism across eight H100s” case.
Runtime memory may additionally include:
- activation tensors;
- KV cache;
- CUDA graphs;
- communication buffers;
- temporary weight-conversion buffers;
- engine metadata;
- allocator fragmentation;
- extra memory for long contexts, batching, or concurrency.
This is why NVIDIA’s same-family TensorRT-LLM guide requires more than the nominal FP8 weight size.
2. Why 8×H200 is more natural
Eight H200 GPUs provide approximately 1.128 TB of aggregate HBM, leaving substantially more room beyond the model weights than eight H100s.
The vLLM Expert Parallel guide provides the following same-family deployment pattern for DeepSeek-V3-0324:
vllm serve deepseek-ai/DeepSeek-V3-0324 \
--tensor-parallel-size 1 \
--data-parallel-size 8 \
--enable-expert-parallel
The documentation says this configuration works on an eight-GPU H200 or H20 node. It also directs H100 users toward a smaller model or the multi-node section.
This is evidence that an 8×H200 route is plausible for a DeepSeek-V3-family MoE model. It is not evidence that the exact same command, container, and defaults have been validated for DeepSeek-Prover-V2-671B.
3. What 16×H100 changes
Sixteen H100s provide enough aggregate memory for the same-family FP8 recommendation in NVIDIA’s guide. In practice, this will often mean two eight-GPU nodes.
A two-node system introduces another set of requirements:
- InfiniBand or a comparable RDMA-capable network;
- GPUDirect RDMA support;
- a suitable NCCL topology;
- identical model paths and software environments on both nodes;
- a distributed runtime configuration;
- enough network performance for tensor/expert communication.
The current vLLM parallelism and scaling documentation explains both 8-GPU-per-node tensor parallel plus two-way pipeline parallel configurations and cross-node diagnostics.
It also suggests checking NCCL logs. A line containing NET/IB/GDRDMA indicates InfiniBand with GPUDirect RDMA, while NET/Socket indicates ordinary TCP sockets, which can be a serious bottleneck for cross-node model parallelism.
4. If only 8×H100 is available
There are community examples of serving related 671B DeepSeek models on a single 8×H100 machine after quantization, such as this DeepSeek-V3/R1 8×H100 deployment and benchmark guide.
There are also community-produced GGUF quantizations of DeepSeek-Prover-V2-671B.
These are useful technical leads, but they do not establish equivalence to the released checkpoint:
- the first project concerns related DeepSeek-V3/R1 models rather than Prover-V2;
- the weight format differs;
- the backend differs;
- theorem-proving accuracy after quantization may behave differently from ordinary conversational quality;
- paper-level result reproduction would require treating quantization as an experimental variable.
I would therefore describe 8×H100 as a quantized, converted, or offloaded route, not as the default route for the released checkpoint.
Backend, parallelism, and interconnect considerations
The backend is part of the hardware requirement
The HF page now exposes basic usage examples for Transformers, vLLM, and SGLang. For example, it shows generic commands such as:
vllm serve "deepseek-ai/DeepSeek-Prover-V2-671B"
and:
python3 -m sglang.launch_server \
--model-path "deepseek-ai/DeepSeek-Prover-V2-671B"
These examples are useful entry points, but the page does not document:
- a validated GPU topology;
- exact vLLM or SGLang versions;
- a tested container digest;
- tensor/data/expert parallel settings;
- expected peak memory;
- expected throughput;
- a tested maximum input/output length;
- the precise checkpoint revision used in validation.
For a small dense model, choosing a backend may mostly be an operational preference. For a 671B MoE model, it changes memory placement and communication behavior.
Tensor parallelism versus expert parallelism
DeepSeek-V3-family models are mixture-of-experts models. Their expert layers can be distributed differently from attention layers.
The vLLM example uses:
- tensor parallel size 1;
- data parallel size 8;
- expert parallelism enabled.
In that arrangement, the attention weights are replicated across the eight processes, while expert weights are distributed across GPUs.
A plain eight-way tensor-parallel configuration and an expert-parallel configuration are therefore not equivalent. They may differ in:
- weight placement;
- KV-cache duplication;
- batch capacity;
- all-to-all communication;
- latency;
- throughput;
- sensitivity to GPU topology.
“Eight GPUs” is not a complete topology
These configurations may all be advertised as “8×H200,” but they need not perform similarly:
- Eight H200 SXM GPUs in one HGX server with NVSwitch.
- Eight PCIe GPUs in one server.
- Two four-GPU servers connected by InfiniBand.
- Two servers connected only by ordinary Ethernet.
- Eight independently scheduled cloud GPUs that are not part of one distributed node.
For this workload, I would ask whether the GPUs are:
- in one physical machine;
- SXM or PCIe;
- connected through NVLink/NVSwitch;
- exposed as one schedulable node;
- backed by InfiniBand/RDMA if multiple nodes are involved.
Useful preflight diagnostics
A provider may already have results for:
nvidia-smi topo -m
For a deeper bandwidth sanity check, NVIDIA maintains:
These tests do not prove that the model will run correctly, but they can reveal that a supposedly high-end distributed configuration is communicating over a much weaker path than expected.
Container pinning
For a paid experiment, I would not rely on an unpinned latest container.
It is better to record:
- image name and digest;
- NVIDIA driver version;
- CUDA version;
- PyTorch version;
- Transformers version;
- vLLM/SGLang/TensorRT-LLM version or commit;
- attention backend;
- all-to-all backend;
- checkpoint commit hash.
This is especially relevant because the project currently has an open question asking for the exact torch, Transformers, FlashAttention, and vLLM versions used by the authors. The existence of the question does not establish that deployment is broken; it shows that the public reproduction environment is not fully pinned in one place.
Managed API, dedicated deployment, or raw GPU node?
These three services solve different problems.
| Access type |
Good fit |
What may be unavailable |
| Serverless API |
Small tests, prompt checks, output parsing, preliminary quality checks |
Exact revision control, custom engine flags, SSH, local Lean integration |
| Managed dedicated deployment |
Larger workloads without managing the serving stack |
Root access, arbitrary containers, low-level backend changes |
| Raw VM or bare-metal node |
Exact checkpoint control, custom serving, local verifier loops |
Setup effort, download time, distributed debugging |
Serverless API
A serverless route is useful when the immediate question is:
Can this model produce useful outputs for my statements, and does my extraction and verification code work?
It is less suitable when the question is:
Can I reproduce the authors’ exact result with the released checkpoint and a known sampling configuration?
The provider may perform internal transformations that are perfectly reasonable for serving but material for reproduction.
For an API route, useful metadata includes:
- source repository and revision;
- reported quantization or precision;
- tokenizer and chat template;
- maximum input and output lengths;
- support for temperature, top-p, seed, stop sequences, and logprobs;
- batching and concurrency limits;
- whether raw assistant output is returned unchanged;
- data-retention policy.
The Novita page currently identifies its endpoint as FP8 and serverless. That makes it a convenient possible smoke-test route, but the page alone does not prove that its internal representation is identical to the files in the HF repository.
Managed dedicated deployment
The Fireworks model page currently identifies the model as available for on-demand deployment on dedicated GPUs and links it to the HF model.
This may be a useful middle ground when:
- the expected workload is larger than an occasional API call;
- predictable capacity is important;
- managing vLLM/SGLang is not the research objective;
- an OpenAI-compatible endpoint is enough.
I would still verify whether the workflow needs anything that an endpoint may not expose, such as:
- custom logits processors;
- custom batching or scheduling;
- direct model-file access;
- experimental engine builds;
- local Lean processes;
- custom verifier-feedback loops;
- deterministic replay of every sampling setting.
Raw node
A raw node is the most flexible route if the work requires:
- an exact HF revision;
- a particular weight conversion;
- custom vLLM/SGLang/TensorRT-LLM builds;
- local Lean and Mathlib installations;
- direct access to all generation logs;
- repeated pass@k experiments;
- custom retry or verifier-feedback logic.
For that route, I would prioritize a provider offering a short test allocation and a prebuilt DeepSeek-family container over a nominally cheaper provider that only guarantees the GPU model.
A practical validation sequence before paying for a long reservation
I would separate validation into stages so that a failure can be attributed to the model host, the serving stack, or the Lean pipeline.
Stage 1: Pin the artifact
Record:
- repository:
deepseek-ai/DeepSeek-Prover-V2-671B;
- exact HF commit or revision;
- original, converted, or quantized weight format;
- checksum or manifest if the provider prepares the files;
- tokenizer revision;
- model configuration revision.
Avoid silently comparing an official-checkpoint run with a GGUF, AWQ, W4A8, or provider-converted run.
Stage 2: Pin the software environment
Record:
- OS/container;
- GPU driver;
- CUDA;
- PyTorch;
- Transformers;
- serving engine and commit;
- FlashAttention/FlashMLA or equivalent backend;
- all-to-all communication backend;
- any custom patches.
A working container digest is more useful than “vLLM latest worked last month.”
Stage 3: Confirm the physical topology
Check:
- all GPUs are visible;
- expected memory is visible;
- NVLink/NVSwitch topology is present;
- local NVMe capacity is adequate;
- multi-node communication is using the intended network;
- host RAM and shared memory are sufficient.
The checkpoint itself is approximately 689 GB, so I would prefer considerably more than 689 GB of usable local storage. Space may also be needed for the HF cache, converted weights, container layers, logs, benchmark data, and duplicate temporary files.
Stage 4: Perform a conservative model load
For the first load:
- use one request at a time;
- use a short input;
- limit the maximum model length if necessary;
- avoid speculative decoding;
- avoid MTP unless specifically required;
- avoid aggressive concurrency;
- preserve complete startup logs.
The goal is only to establish:
- the model loads;
- one deterministic request completes;
- the output is not truncated or corrupted;
- memory use is observable.
Optimization features can be added one at a time later.
Stage 5: Run a Lean-aware smoke test
Use a few fixed formal statements and save:
- the exact prompt;
- raw token/text output;
- sampling parameters;
- model and tokenizer revisions;
- extracted Lean code;
- compiler output;
- timeout result.
A generated proof-looking string is not yet a successful theorem-proving result. The useful endpoint of the test is a proof accepted by the intended Lean environment.
Stage 6: Run a small sampling test
Before a large pass@k experiment, try a small fixed sample budget—for example, enough to observe:
- generation length distribution;
- duplicate-output rate;
- Lean compilation rate;
- timeout rate;
- out-of-memory rate;
- effective output tokens per second;
- successful verified proofs per hour.
Then increase only one variable at a time:
- context length;
- maximum output length;
- batch size;
- concurrency;
- sample budget.
Stage 7: Estimate cost from verified work
GPU-hour price alone is not the most informative metric for this workload.
A more useful estimate is based on:
number of problems
× samples per problem
× average generated tokens
÷ effective generation throughput
× node-hour price
Then add:
- model download and conversion time;
- container startup;
- failed or interrupted jobs;
- verifier time;
- persistent storage;
- idle time between generation and verification.
For theorem proving, I would ultimately compare verified proofs per hour or cost per verified proof, not only tokens per second.
Serving the model is not the same as reproducing the reported evaluation
The distinction matters here because the published evaluation uses large sampling budgets and a specific Lean environment.
The current DeepSeek-Prover-V2 paper states that its experiments used Lean 4.9.0-rc2 and a revised MiniF2F environment. It reports evaluations at sample budgets including Pass@32, Pass@1024, and Pass@8192, depending on the benchmark.
For MiniF2F, the paper reports an average output length of approximately:
- 762 tokens for the 671B non-CoT mode;
- 6,752 tokens for the 671B CoT mode.
That difference alone can substantially change runtime and cost.
The authors’ repository also currently has an open issue requesting the pass@k inference hyperparameters. Therefore, someone attempting exact reproduction may still need to resolve or choose:
- temperature;
- top-p;
- maximum output length;
- stop conditions;
- number of samples;
- prompt mode;
- seed behavior;
- duplicate handling;
- timeout and retry behavior.
This does not mean that useful experiments cannot be performed. It means that “I served the model successfully” and “I reproduced the published pass@k result” should be recorded as different claims.
Lean environment details worth pinning
At minimum:
- Lean toolchain version;
- Mathlib revision;
- benchmark revision;
- imports;
- namespaces;
maxHeartbeats;- process timeout;
- memory limit;
- extraction of Lean code from mixed natural-language/Lean output;
- treatment of
sorry, admit, axioms, and unexpected declarations.
There is also a community report about a published/example proof not compiling in the reporter’s environment. That report does not identify a universal root cause: differences in Lean, Mathlib, imports, benchmark revisions, or copied text could all matter. It is mainly another reason to save the exact environment and compiler output.
The revised paper itself discusses a corrected result related to a Lean 4.9.0 user-interface bug. That is a useful reminder that kernel acceptance, tactic behavior, benchmark formulation, and the intended mathematical statement are separate layers of validation.
Optional control: validate the pipeline with a smaller prover first
If the research question is specifically about the 671B model, a smaller model is not a substitute.
However, a smaller prover can be a useful control for validating everything around the expensive model:
- benchmark loading;
- prompt construction;
- output extraction;
- Lean invocation;
- compiler timeouts;
- result storage;
- pass@k aggregation;
- failure classification.
Possible controls include the official DeepSeek-Prover-V2-7B model or a later open prover such as Goedel-Prover-V2.
A smaller control can answer:
Does my evaluation pipeline work?
It cannot answer:
Does the 671B checkpoint have the same behavior, quality, sample efficiency, or sensitivity to quantization?
This separation may prevent expensive GPU time from being spent debugging a Lean version mismatch or an output-parser bug.
Condensed recommendation
If I were choosing a route from the currently visible information, I would use this order:
- Smoke-test the exact model name through a managed API/deployment, if that is acceptable.
- Confirm that the prompt, output extraction, and Lean verification pipeline work on a few fixed problems.
- For self-hosting the released checkpoint, look for a single 8×H200 SXM/NVLink or 8×B200 node with a known-good container and a short validation period.
- Treat 16×H100 as a plausible same-family FP8 route, but verify multi-node networking carefully.
- Treat 8×H100 as the quantized/converted/offloaded branch unless a provider can demonstrate a reproducible configuration for the released weights.
- Scale to a long run only after measuring actual generation length, verified-proof throughput, and failure rate.
The two highest-value details to establish are therefore not just “which GPU is available,” but:
- whether the released checkpoint must be preserved, or quantization/conversion is acceptable;
- whether the required interface is an API, a managed dedicated endpoint, or a raw SSH-accessible node.
Those two choices should narrow the server search considerably and reduce the risk of paying for a configuration that can load a related DeepSeek model but does not support the intended theorem-proving experiment.