Hi all,
I’m a computer science student in Italy working on AI for formal reasoning: theorem proving in Lean, proof search, model checking, and long-running local reasoning agents. It’s a fairly underrepresented niche in the local-LLM space, and DGX Spark looks like the ideal machine to do it on.
The ask, up front
I’m asking whether NVIDIA could provide a DGX Spark unit (128 GB unified memory) free of charge, as a sponsorship for an independent student researcher. I’m not in a position to buy one. A donated or sponsored unit, an early-access slot, or an academic/developer program would all work. If there’s a proper channel or contact for this kind of request, please point me to it.
What I’m building
Local agentic pipelines that pair LLMs with formal tools for automated reasoning, running fully offline and reproducibly: models that explore definitions, lemmas, proofs, and counterexamples, with the heavy lifting kept on local hardware rather than an API.
The model stack I want to run
The core idea is a multi-model setup, all resident at once, each playing a role:
- Reasoner / orchestrator: gpt-oss-120b (MoE, MXFP4). Drives the agent, plans the proof strategy, decomposes goals. MoE keeps generation fast on Spark’s memory bandwidth.
- Dedicated Lean prover: DeepSeek-Prover-V2 (with Goedel-Prover / Kimina-Prover as alternatives to benchmark). Small, specialized, state-of-the-art at closing Lean goals, leaving most of the memory free.
- Coder: a Qwen3-Coder class model for tactic synthesis and tooling code.
- Optional heavier reasoner: Qwen3-235B-A22B at 4-bit, for the hard goals where raw model quality matters more than latency.
Running a large reasoner, a specialized prover, and a coder simultaneously, with room left for long agentic context, is exactly what 128 GB of unified memory enables and what a single consumer GPU cannot do. On Spark I can keep all of them warm and let the agent route between them instead of constantly swapping weights.
Where I am now (RTX 5080 laptop)
My current setup works for getting started, but the real limit is memory, not raw speed. The models that genuinely help on hard proofs are too large to fit comfortably, and I can’t keep a capable reasoner and a dedicated prover loaded at the same time, so the agent ends up swapping models instead of working. Long reasoning sessions also tend to run out of room before the search gets anywhere. This is exactly the ceiling the 128 GB of unified memory would remove.
What I’d contribute back
In return for a sponsored unit, I’d run open, reproducible benchmarks on DGX Spark and publish them on GitHub, with evaluation scripts anyone can rerun and NVIDIA credited. Rather than deciding the scope alone, I’d rather ask:
What would you actually want to see benchmarked on a Spark? Which models, which Lean problem sets or reasoning tasks, single vs multi-model setups, long-context behavior? Tell me what would be useful and I’ll prioritize it.
(I’d stick to public models and public problem sets, so everything stays fully shareable.)
Happy to hop on a quick call if needed. Thanks!
Pietro Pellegrino
GitHub: shalashaska117 (Pietro) · GitHub
LinkedIn: https://www.linkedin.com/in/ppellegrino2002/