bfs-prover-v2-32b

<div align="center">

🔬 BFS-Prover-V2 32B - GGUF

Formal Mathematical Proof Generation for Lean4

Original Model | Ollama Registry | 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:

# 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:

# 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:

# 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

💡 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:

Variant Details

📚 Usage Examples

Theorem Proving

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

Proof State Completion

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

Interactive Proving

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

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

# 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:

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:

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 for creating BFS-Prover-V2
• GGUF Format: Georgi Gerganov for llama.cpp
• Ollama: Ollama team 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
• 🚀 Ollama Registry: richardyoung/bfs-prover-v2-32b
• 🛠️ llama.cpp: GitHub
• 📖 Lean4 Documentation: Lean Community
• 💬 Discussions: Ask questions here!

📚 Citation

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

@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:

-- 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:

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

3. Batch Proof Generation

Process multiple theorems:

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:

# 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">

Built & maintained by Richard Young · DeepNeuro 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:

Recommended Setups

Use Case

This model excels at:

• Lean4 theorem proving
• Formal mathematical proofs
• Proof search and verification