Instructions to use mradermacher/BFS-Prover-GGUF with libraries, inference providers, notebooks, and local apps. Follow these links to get started.

Libraries

How to use mradermacher/BFS-Prover-GGUF with Transformers:

# pip install -U transformers accelerate
# Load model directly
from transformers import AutoModel
model = AutoModel.from_pretrained("mradermacher/BFS-Prover-GGUF", device_map="auto")

Notebooks
Google Colab
Kaggle
Local Apps Settings

llama.cpp

How to use mradermacher/BFS-Prover-GGUF with llama.cpp:

Install (macOS, Linux)

curl -LsSf https://llama.app/install.sh | sh
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf mradermacher/BFS-Prover-GGUF:Q4_K_M
# Run inference directly in the terminal:
llama cli -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Install from WinGet (Windows)

winget install llama.cpp
# Start a local OpenAI-compatible server with a web UI:
llama serve -hf mradermacher/BFS-Prover-GGUF:Q4_K_M
# Run inference directly in the terminal:
llama cli -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Use pre-built binary

# Download pre-built binary from:
# https://github.com/ggerganov/llama.cpp/releases
# Start a local OpenAI-compatible server with a web UI:
./llama-server -hf mradermacher/BFS-Prover-GGUF:Q4_K_M
# Run inference directly in the terminal:
./llama-cli -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Build from source code

git clone https://github.com/ggerganov/llama.cpp.git
cd llama.cpp
cmake -B build
cmake --build build -j --target llama-server llama-cli
# Start a local OpenAI-compatible server with a web UI:
./build/bin/llama-server -hf mradermacher/BFS-Prover-GGUF:Q4_K_M
# Run inference directly in the terminal:
./build/bin/llama-cli -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Use Docker

docker model run hf.co/mradermacher/BFS-Prover-GGUF:Q4_K_M

LM Studio
Jan
Ollama
How to use mradermacher/BFS-Prover-GGUF with Ollama:
```
ollama run hf.co/mradermacher/BFS-Prover-GGUF:Q4_K_M
```
Unsloth Desktop

How to use mradermacher/BFS-Prover-GGUF with Pi:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Configure the model in Pi

# Install Pi:
npm install -g @earendil-works/pi-coding-agent
# Add to ~/.pi/agent/models.json:
{
  "providers": {
    "llama-cpp": {
      "baseUrl": "http://localhost:8080/v1",
      "api": "openai-completions",
      "apiKey": "none",
      "models": [
        {
          "id": "mradermacher/BFS-Prover-GGUF:Q4_K_M"
        }
      ]
    }
  }
}

Run Pi

# Start Pi in your project directory:
pi

Docker Model Runner
How to use mradermacher/BFS-Prover-GGUF with Docker Model Runner:
```
docker model run hf.co/mradermacher/BFS-Prover-GGUF:Q4_K_M
```

Lemonade

How to use mradermacher/BFS-Prover-GGUF with Lemonade:

Pull the model

# Download Lemonade from https://lemonade-server.ai/
lemonade pull mradermacher/BFS-Prover-GGUF:Q4_K_M

Run and chat with the model

lemonade run user.BFS-Prover-GGUF-Q4_K_M

List all available models

lemonade list

Hermes Agent

How to use mradermacher/BFS-Prover-GGUF with Hermes Agent:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Configure Hermes

# Install Hermes:
curl -fsSL https://hermes-agent.nousresearch.com/install.sh | bash
hermes setup
# Point Hermes at the local server:
hermes config set model.provider custom
hermes config set model.base_url http://127.0.0.1:8080/v1
hermes config set model.default mradermacher/BFS-Prover-GGUF:Q4_K_M

Run Hermes

hermes

Atomic Chat

OpenClaw

How to use mradermacher/BFS-Prover-GGUF with OpenClaw:

Start the llama.cpp server

# Install llama.cpp:
brew install llama.cpp
# Start a local OpenAI-compatible server:
llama serve -hf mradermacher/BFS-Prover-GGUF:Q4_K_M

Configure OpenClaw

# Install OpenClaw:
npm install -g openclaw@latest
# Register the local server and set it as the default model:
openclaw onboard --non-interactive --mode local \
  --auth-choice custom-api-key \
  --custom-base-url http://127.0.0.1:8080/v1 \
  --custom-model-id "mradermacher/BFS-Prover-GGUF:Q4_K_M" \
  --custom-provider-id llama-cpp \
  --custom-compatibility openai \
  --custom-text-input \
  --accept-risk \
  --skip-health

Run OpenClaw

openclaw agent --local --agent main --message "Hello from Hugging Face"

mradermacher commited on Oct 12, 2025

Commit

6f69f43

verified ·

1 Parent(s): cbac5ee

auto-patch README.md

Browse files

Files changed (1) hide show

README.md +7 -2

README.md CHANGED Viewed

@@ -1,5 +1,5 @@
 ---
-base_model: ByteDance-Seed/BFS-Prover
 datasets:
 - internlm/Lean-Workbook
 - internlm/Lean-Github
@@ -8,6 +8,8 @@ language:
 - en
 library_name: transformers
 license: apache-2.0
 quantized_by: mradermacher
 tags:
 - lean4
@@ -21,9 +23,12 @@ tags:
 <!-- ### convert_type: hf -->
 <!-- ### vocab_type:  -->
 <!-- ### tags:  -->
-static quants of https://huggingface.co/ByteDance-Seed/BFS-Prover
 <!-- provided-files -->
 weighted/imatrix quants seem not to be available (by me) at this time. If they do not show up a week or so after the static ones, I have probably not planned for them. Feel free to request them by opening a Community Discussion.
 ## Usage

 ---
+base_model: ByteDance-Seed/BFS-Prover-V1-7B
 datasets:
 - internlm/Lean-Workbook
 - internlm/Lean-Github
 - en
 library_name: transformers
 license: apache-2.0
+mradermacher:
+  readme_rev: 1
 quantized_by: mradermacher
 tags:
 - lean4
 <!-- ### convert_type: hf -->
 <!-- ### vocab_type:  -->
 <!-- ### tags:  -->
+static quants of https://huggingface.co/ByteDance-Seed/BFS-Prover-V1-7B
 <!-- provided-files -->
+***For a convenient overview and download list, visit our [model page for this model](https://hf.tst.eu/model#BFS-Prover-GGUF).***
 weighted/imatrix quants seem not to be available (by me) at this time. If they do not show up a week or so after the static ones, I have probably not planned for them. Feel free to request them by opening a Community Discussion.
 ## Usage