---
license: apache-2.0
base_model: ByteDance-Seed/BFS-Prover-V2-32B
pipeline_tag: text-generation
library_name: llama.cpp
language:
  - en
tags:
  - gguf
  - quantized
  - ollama
  - llama-cpp
  - qwen2.5
  - formal-verification
  - theorem-proving
  - lean4
  - mathematics
  - proof-generation
quantized_by: richardyoung
---

<div align="center">

# 🔬 BFS-Prover-V2 32B - GGUF

### Formal Mathematical Proof Generation for Lean4

[![GGUF](https://img.shields.io/badge/Format-GGUF-blue)](https://github.com/ggerganov/llama.cpp)
[![Size](https://img.shields.io/badge/Variants-3_Quantizations-green)](https://huggingface.co/richardyoung/bfs-prover-v2-32b)
[![Ollama](https://img.shields.io/badge/Runtime-Ollama-orange)](https://ollama.ai/)
[![License](https://img.shields.io/badge/License-Apache_2.0-blue.svg)](https://opensource.org/licenses/Apache-2.0)
[![Context](https://img.shields.io/badge/Context-131K_tokens-purple)](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)

**[Original Model](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)** | **[Ollama Registry](https://ollama.com/richardyoung/bfs-prover-v2-32b)** | **[llama.cpp](https://github.com/ggerganov/llama.cpp)**

---

</div>

## 📖 What is This?

This is **BFS-Prover-V2 32B**, a specialized 32-billion parameter model fine-tuned for **formal mathematical proof generation** and **theorem proving** in Lean4. Quantized to **GGUF format** for efficient local inference with Ollama or llama.cpp!

### ✨ Why You'll Love It

- 🔬 **Formal Verification** - Generates valid Lean4 proofs
- 🧮 **Mathematical Reasoning** - Deep understanding of mathematical concepts
- 📚 **131K Context** - Handle complex proof sequences and large mathematical contexts
- ⚡ **Local Inference** - Run entirely on your machine, no API calls
- 🔒 **Privacy First** - Your proofs never leave your computer
- 🎯 **Multiple Quantizations** - Choose your speed/quality trade-off
- 🚀 **Ollama Ready** - One command to start proving theorems
- 🔧 **llama.cpp Compatible** - Works with your favorite tools

## 🎯 Quick Start

### Option 1: Ollama (Easiest!)

Pull and run directly from the Ollama registry:

```bash
# Recommended: Q5_K_M (best balance)
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M

# Other variants
ollama run richardyoung/bfs-prover-v2-32b:Q6_K    # Highest quality
ollama run richardyoung/bfs-prover-v2-32b:Q4_K_M  # Faster, smaller
```

That's it! Start proving theorems! 🎉

### Option 2: Build from Modelfile

Download this repo and build locally:

```bash
# Clone or download the modelfiles
ollama create bfs-prover-v2-q5 -f modelfiles/bfs-prover-v2-32b--Q5_K_M.Modelfile
ollama run bfs-prover-v2-q5
```

### Option 3: llama.cpp

Use with llama.cpp directly:

```bash
# Download the GGUF file (replace variant as needed)
huggingface-cli download richardyoung/bfs-prover-v2-32b BFS-Prover-V2-32B-Q5_K_M.gguf --local-dir ./

# Run with llama.cpp
./llama-cli -m BFS-Prover-V2-32B-Q5_K_M.gguf -p "theorem add_comm (a b : Nat) : a + b = b + a :::"
```

## 💻 System Requirements

| Component | Minimum | Recommended |
|-----------|---------|-------------|
| **RAM** | 24 GB | 32 GB+ |
| **Storage** | 30 GB free | 40+ GB free |
| **CPU** | Modern 8-core | 16+ cores |
| **GPU** | Optional (CPU-only works!) | Metal/CUDA for acceleration |
| **OS** | macOS, Linux, Windows | Latest versions |

> 💡 **Tip:** Larger quantizations (Q6_K) need more RAM but produce better proofs. Smaller ones (Q4_K_M) are faster but less precise.

## 🎨 Available Quantizations

Choose the right balance for your needs:

| Quantization | Size | Quality | Speed | RAM Usage | Best For |
|--------------|------|---------|-------|-----------|----------|
| **Q6_K** | 27 GB | ⭐⭐⭐⭐⭐ | ⭐⭐⭐ | ~32 GB | Production proofs, research |
| **Q5_K_M** (recommended) | 23 GB | ⭐⭐⭐⭐ | ⭐⭐⭐⭐ | ~28 GB | Daily use, best balance |
| **Q4_K_M** | 19 GB | ⭐⭐⭐ | ⭐⭐⭐⭐⭐ | ~24 GB | Quick iteration, constrained systems |

### Variant Details

| Variant | Size | Context | Best For |
|---------|------|---------|----------|
| `Q6_K` | 27 GB | 131K | Highest quality, complex proofs |
| `Q5_K_M` | 23 GB | 131K | Recommended for most users |
| `Q4_K_M` | 19 GB | 131K | Faster inference, lower memory |

## 📚 Usage Examples

### Theorem Proving

```bash
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "theorem add_comm (a b : Nat) : a + b = b + a :::"
```

### Proof State Completion

```bash
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "∀ n : Nat, n + 0 = n :::"
```

### Interactive Proving

```bash
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M
>>> theorem zero_add (n : Nat) : 0 + n = n :::
>>> lemma succ_eq_add_one (n : Nat) : Nat.succ n = n + 1 :::
```

### Using with Python

```python
import requests
import json

def prove_lean4(theorem_statement):
    response = requests.post('http://localhost:11434/api/generate',
        json={
            'model': 'richardyoung/bfs-prover-v2-32b:Q5_K_M',
            'prompt': f'{theorem_statement} :::',
            'stream': False
        })
    return response.json()['response']

# Example
proof = prove_lean4("theorem add_zero (n : Nat) : n + 0 = n")
print(proof)
```

## 🏗️ Model Details

<details>
<summary><b>Click to expand technical details</b></summary>

### Architecture

- **Base Model:** BFS-Prover-V2-32B by ByteDance-Seed
- **Architecture:** Qwen2.5-32B
- **Parameters:** 32 Billion
- **Context Length:** 131,072 tokens (131K)
- **Quantization:** GGUF format (Q4_K_M to Q6_K)
- **Optimization:** Formal mathematical proof generation
- **Training:** Specialized for Lean4 theorem proving

### Specialization

The model excels at:
- **Lean4 Theorem Proving** - Generate formal proofs
- **Proof Completion** - Complete partial proof states
- **Mathematical Formalization** - Translate informal math to formal statements
- **Tactic Generation** - Suggest proof tactics for given goals
- **Proof Search** - Explore proof spaces using BFS (Breadth-First Search)

### Prompt Format

The model uses a special format where proof requests end with `:::`:

```
theorem add_comm (a b : Nat) : a + b = b + a :::
```

This signals the model to generate a formal proof for the given theorem statement.

</details>

## ⚡ Performance Tips

<details>
<summary><b>Getting the best results</b></summary>

1. **Choose the right quantization** - Q5_K_M is recommended for daily use
2. **Use proper Lean4 syntax** - Follow standard Lean4 theorem statement format
3. **Include the ::: suffix** - This is critical for the model to understand you want a proof
4. **Set low temperature** - Use 0.1-0.3 for precise, valid proofs
5. **Provide context** - Include relevant definitions or prior lemmas
6. **GPU acceleration** - Use Metal (Mac) or CUDA (NVIDIA) for faster inference
7. **Large context** - Take advantage of the 131K context for complex proofs

### Example Ollama Configuration

```bash
# Create with custom parameters
ollama create my-bfs-prover -f modelfiles/bfs-prover-v2-32b--Q5_K_M.Modelfile

# Edit the Modelfile to add:
PARAMETER temperature 0.2
PARAMETER top_p 0.95
PARAMETER num_ctx 131072
```

</details>

## 🔧 Building Custom Variants

You can modify the included Modelfiles to customize behavior:

```dockerfile
FROM ./BFS-Prover-V2-32B-Q5_K_M.gguf

# Lean4-specific prompt template (appends ::: to user messages)
TEMPLATE """{{- range $i, $m := .Messages }}{{- if eq $m.Role "user" }}{{ $m.Content }}:::{{ end }}{{- if eq $m.Role "assistant" }}{{ $m.Content }}{{ end }}{{- end }}"""

# System prompt
SYSTEM You are a formal mathematics expert specializing in Lean4 theorem proving. Generate valid, well-structured proofs.

# Parameters
PARAMETER temperature 0.2
PARAMETER num_ctx 131072
```

Then build:

```bash
ollama create my-custom-prover -f custom.Modelfile
```

## 🎓 Use Cases

- 📐 **Mathematical Research** - Formalize and verify mathematical theorems
- 🏫 **Education** - Learn formal mathematics and proof techniques
- 🔍 **Proof Exploration** - Discover new proof strategies
- ✅ **Verification** - Verify correctness of mathematical statements
- 📚 **Library Building** - Contribute to Lean4 mathematical libraries
- 🤖 **Automated Reasoning** - Build automated theorem proving systems

## ⚠️ Known Limitations

- 💾 **Large Size** - Even the smallest variant needs 19+ GB of storage
- 🐏 **RAM Intensive** - Requires significant system memory (24+ GB)
- ⏱️ **Inference Speed** - Slower than smaller models (trade-off for quality)
- 🌐 **English-Focused** - Best performance with English mathematical language
- 📝 **Lean4-Specialized** - Optimized specifically for Lean4, not general math
- 🎯 **Proof Format** - Requires proper Lean4 syntax and ::: suffix

## 📄 License

Apache 2.0 - Same as the original model. Free for commercial use!

## 🙏 Acknowledgments

- **Original Model:** [ByteDance-Seed](https://huggingface.co/ByteDance-Seed) for creating BFS-Prover-V2
- **GGUF Format:** [Georgi Gerganov](https://github.com/ggerganov) for llama.cpp
- **Ollama:** [Ollama team](https://ollama.ai/) for the amazing runtime
- **Lean Community:** All the mathematicians and developers working on formal verification

## 🔗 Useful Links

- 📦 **Original Model:** [ByteDance-Seed/BFS-Prover-V2-32B](https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B)
- 🚀 **Ollama Registry:** [richardyoung/bfs-prover-v2-32b](https://ollama.com/richardyoung/bfs-prover-v2-32b)
- 🛠️ **llama.cpp:** [GitHub](https://github.com/ggerganov/llama.cpp)
- 📖 **Lean4 Documentation:** [Lean Community](https://lean-lang.org/)
- 💬 **Discussions:** [Ask questions here!](https://huggingface.co/richardyoung/bfs-prover-v2-32b/discussions)

## 📚 Citation

If you use this model in your research, please cite:

```bibtex
@misc{bfs-prover-v2-2024,
  title={BFS-Prover-V2: Formal Mathematical Proof Generation},
  author={ByteDance-Seed Team},
  year={2024},
  url={https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B}
}
```

## 🎮 Pro Tips

<details>
<summary><b>Advanced usage patterns</b></summary>

### 1. Integration with Lean4 IDE

Use with Lean4 VSCode extension for interactive proving:

```lean4
-- Use the model to suggest proof tactics
theorem my_theorem : ∀ n : Nat, n + 0 = n := by
  -- Query model for tactics
  sorry
```

### 2. API Server Mode

Run as an OpenAI-compatible API:

```bash
ollama serve
# Then use the API at http://localhost:11434
```

### 3. Batch Proof Generation

Process multiple theorems:

```bash
for theorem in theorems.txt; do
  ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "$theorem :::" >> proofs.txt
done
```

### 4. Chain-of-Thought Proving

Break complex proofs into steps:

```bash
# Step 1: Generate high-level strategy
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "Outline proof strategy for: theorem_statement :::"

# Step 2: Generate detailed proof
ollama run richardyoung/bfs-prover-v2-32b:Q5_K_M "Complete proof: theorem_statement :::"
```

</details>

---

<div align="center">

**Quantized with ❤️ by [richardyoung](https://deepneuro.ai/richard)**

*If you find this useful, please ⭐ star the repo and share with other mathematicians!*

**Format:** GGUF | **Runtime:** Ollama / llama.cpp | **Created:** October 2025

</div>


## Hardware Requirements

BFS-Prover-V2 is a 32B model specialized for formal theorem proving in Lean4:

| Quantization | Model Size | VRAM Required | Quality |
|:------------:|:----------:|:-------------:|:--------|
| **Q3_K_M** | ~15 GB | 18 GB | Good |
| **Q4_K_M** | ~19 GB | 24 GB | Very Good - recommended |
| **Q5_K_M** | ~23 GB | 28 GB | Excellent |
| **Q6_K** | ~27 GB | 32 GB | Near original |
| **Q8_0** | ~35 GB | 40 GB | Original quality |

### Recommended Setups

| Hardware | Recommended Quantization |
|:---------|:-------------------------|
| RTX 4090 (24GB) | Q4_K_M |
| RTX 3090 (24GB) | Q4_K_M |
| A100 (40GB) | Q8_0 |
| Mac M2 Ultra (192GB) | Q8_0 |

### Use Case

This model excels at:
- Lean4 theorem proving
- Formal mathematical proofs
- Proof search and verification