Más allá de ser simples asistentes de uso cotidiano, la inteligencia artificial está transformando los campos de las ciencias y las matemáticas. Un ejemplo claro de esto es el uso de modelos de lenguajes avanzados como DeepSeek Prover V2, aplicado en la demostración formal de teoremas matemáticos y problemas complejos. Este LLM está diseñado para trabajar con Lean 4 en entornos Linux, pero también es posible instalarlo y ejecutarlo en Windows. Si te interesa experimentar con esta potente IA, aquí te mostramos cómo puedes empezar a usarla desde tu PC con Windows.

Puntos Clave:

  1. DeepSeek Prover V2 es una IA especializada en pruebas matemáticas formales mediante el uso de Lean 4.
  2. Para ejecutarla en Windows, es necesario utilizar el Subsistema de Windows para Linux (WSL).
  3. Este LLM requiere de un hardware potente, como una GPU con 32 GB de VRAM y al menos 64 GB de RAM.

¿Trabajas en investigación, ciencia de datos o con matemáticas avanzadas? En este tutorial te mostramos cómo puedes aprovechar todas las capacidades de DeepSeek Prover V2 7b en entornos con Windows 10 o Windows 11.

Qué es y para qué se usa DeepSeek Prover V2

DeepSeek Prover V2 es un modelo de lenguaje de gran escala (LLM) diseñado específicamente para generar demostraciones matemáticas formales utilizando el lenguaje Lean 4. Este lenguaje no solo permite expresar pruebas matemáticas de forma precisa, sino que también actúa como un entorno interactivo para verificar su validez paso a paso.

La versión 7B que vemos en esta guía ofrece el mejor equilibrio entre eficiencia y rendimiento, por lo que es ideal para investigadores que cuentan con recursos limitados, aunque aun así requiere de un PC bastante potente.

Gracias al aprendizaje por refuerzo, DeepSeek mejora continuamente su capacidad de razonar y conectar matemáticas formales e informales, destacando en evaluaciones como MiniF2F y PutnamBench. Así, a diferencia de otros LLM gratuitos accesibles desde el navegador web o una app, como ChatGPT o Perplexity, este modelo es una herramienta más confiable para trabajar en lógica matemática o desarrollo de software.

Cuáles son los requisitos para ejecutar DeepSeek Prover V2 7B en Windows

Si quieres ejecutar este LLM en tu equipo con Windows, necesitas contar con estos requisitos mínimos de hardware y software:

  • Sistema operativo: Windows 10 u 11 con el Subsistema de Windows para Linux (WSL).

  • GPU: NVIDIA RTX A6000 o equivalente, con al menos 32 GB de VRAM.

  • Memoria RAM: 64 GB.

  • Procesador: Intel i7/i9 o AMD Ryzen 7/9 de última generación.

  • Espacio disponible: 100 GB libres en disco.

Cómo instalar y ejecutar DeepSeek Prover V2 7B en Windows

Como anticipamos, este modelo no puede instalarse directamente en Windows, por lo que es necesario configurar un entorno Linux dentro del sistema operativo usando WSL. Así podrás ejecutar distribuciones de Linux de forma nativa sin una máquina virtual. Además, tendrás que instalar el gestor de entornos Conda si aún no lo has hecho.

Aquí te mostramos los pasos en detalle:

  1. Entra al menú inicio, busca “cmd” y haz clic en “Ejecutar como administrador” para abrir el Símbolo del sistema.

  1. Ingresa este comando y envíalo con la tecla Enter para instalar el Subsistema de Windows para Linux:

wsl --install

  1. Una vez completado el proceso, instala Ubuntu con este comando:

wsl --install -d Ubuntu

  1. La distribución de Linux se descargará e instalará automáticamente. Ahora, dirígete a la página de descargas de Anaconda y descarga una versión de la plataforma compatible con tu equipo, puede ser Anaconda o Miniconda.

  1. Una vez instalado Anaconda, abre la terminal de Ubuntu en WSL o Anaconda Prompt desde el menú Inicio y ejecuta este comando para crear el entorno necesario de Python:

conda create -n deepseek python=3.11

  1. Tras crearlo, activa el entorno con el siguiente comando:

conda activate deepseek

  1. Para instalar las dependencias necesarias (PyTorch con soporte CUDA, librerías de procesamiento multimedia y las herramientas requeridas para ejecutar DeepSeek), envía estos comandos uno a la vez:

pip install torch torchvision torchaudio --extra-index-url https://download.pytorch.org/whl/cu117

pip install "transformers>=4.38.0" "accelerate>=0.25.0" "bitsandbytes>=0.41.0" einops

conda install -c conda-forge notebook ipywidgets -y

  1. Para descargar DeepSeek, tienes que abrir un cuaderno de Jupyter Notebook. Desde Anaconda Prompt solo basta con ejecutar el comando “jupyter notebook” (con el entorno Conda previamente activado). Si estás usando Ubuntu en WSL, envía el comando “jupyter notebook --no-browser --ip=127.0.0.1” y luego copia la URL que aparece en la consola y ábrela en tu navegador web.

  2. En el cuaderno, ejecuta el siguiente script que descargará el modelo y el tokenizador desde Hugging Face. También va a configurar automáticamente su ejecución en GPU o CPU según la disponibilidad:

from transformers import AutoModelForCausalLM, AutoTokenizer

import torch

model_id = "deepseek-ai/DeepSeek-Prover-V2-7B"

tokenizer = AutoTokenizer.from_pretrained(model_id)

model = AutoModelForCausalLM.from_pretrained(

model_id,

device_map="auto",

torch_dtype=torch.bfloat16,

trust_remote_code=True

)

  1. Finalmente, hay que probar que todo funciona correctamente con un script para que la IA resuelva una operación matemática básica, como la siguiente:

input_text = "What is the square root of 144?"

inputs = tokenizer(input_text, return_tensors="pt").to(model.device)

outputs = model.generate(**inputs, max_length=512)

print(tokenizer.decode(outputs[0], skip_special_tokens=True))

Si has configurado todo siguiendo bien los pasos, deberías ver la respuesta de la IA con el razonamiento paso a paso para resolver el problema indicado.

Conclusiones personales

Explorar modelos avanzados como DeepSeek Prover V2 abre un mundo de posibilidades para quienes necesitan trabajar con demostraciones matemáticas o automatizaciones. Gracias a su integración en Windows a través de WSL, más usuarios tienen acceso a esta herramienta incluso aunque no cuentan con un PC o VM con Linux.

Si bien el proceso de instalación puede parecer complejo, lo cierto es que si sigues los pasos con cuidado puedes hacer uso de la IA avanzada aunque no tengas experiencia previa en sistemas Unix o LLMs.