Goedel-Prover-V2-32B-GGUF on Win11 + RTX4000 Ada

Download llama.cpp and install the corresponding CUDA runtime. The installed CUDA runtime version must match the one llama.cpp was compiled against.

# Disable progress bar for faster download
$ProgressPreference = 'SilentlyContinue'

# Download the ZIP as a stream and open it as a ZipArchive
$response = Invoke-WebRequest "https://github.com/ggml-org/llama.cpp/releases/download/b6374/llama-b6374-bin-win-cuda-12.4-x64.zip" -UseBasicParsing

Add-Type -AssemblyName System.IO.Compression.FileSystem
$stream = New-Object System.IO.MemoryStream ($response.Content)
$zip    = New-Object System.IO.Compression.ZipArchive($stream)

# Extract directly into the current directory
$zip.ExtractToDirectory((Get-Location).Path)

# Change into the extracted folder
Set-Location ".\llama-b6374-bin-win-cuda-12.4-x64"

# Download the CUDA 12.4.0 local installer to the current directory
Invoke-WebRequest "https://developer.download.nvidia.com/compute/cuda/12.4.0/local_installers/cuda_12.4.0_551.61_windows.exe" -OutFile "cuda_12.4.0_551.61_windows.exe"

# Silent install (includes CUDA runtime) and suppress automatic reboot (-n)
#    -s = silent
#    -n = no automatic reboot after install
Start-Process -FilePath ".\cuda_12.4.0_551.61_windows.exe" -ArgumentList "-s -n" -Wait -NoNewWindow

Restart powershell to reload the environment variables.
Run nvcc --version to check CUDA runtime version.
Run ./llama-server --list-devices to see if there is:

load_backend: loaded CUDA backend from C:\llama.cpp\ggml-cuda.dll

Start the llama-server with:

.\llama-server.exe -m .\Goedel-Prover-V2-32B.Q4_K_M.gguf -t 20 --ctx-size 8192 -ngl 999 --port 8388 --host 0.0.0.0

Official test prompt:

Complete the following Lean 4 code:

```lean4
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat


theorem square_equation_solution {x y : ℝ} (h : x^2 + y^2 = 2*x - 4*y - 5) : x + y = -1 := by
  sorry
```

Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.

Run nvidia-smi -l 1 to see GPU and VRAM usage.

Model files can be found here:

References:

https://huggingface.co/unsloth/Qwen3-30B-A3B-GGUF/resolve/main/Qwen3-30B-A3B-UD-Q4_K_XL.gguf

rikka0w0/win11-cuda-llamacpp-goedel-prover-v2.md