BFS-Prover-V2

Stream: Machine Learning for Theorem Proving

[Ivan Eric]

The latest tactic generator model by ByteDance based on Qwen2.5. It gets 95 % on the miniF2F benchmark

[Ivan Eric]

https://huggingface.co/ByteDance-Seed/BFS-Prover-V2-32B

[Joachim Breitner]

Looks interesting, has someone here tried to use it already?

[(deleted)]

How about you use it

[(deleted)]

I expect the model to be fast

[(deleted)]

If it's slow it's not worth using, but I think it should be fast

[Joachim Breitner]

I’m hardly ever proving things these days :shrug:

[Zeyu Zheng]

Huỳnh Trần Khanh said:

How about you use it

Hi! You can try out our model through LLMLean following the instructions at https://bfs-prover.github.io/V2/

[Bas Spitters]

Looks exciting!
How does LLMLean compare to Lean-LSP-MCP? And how does Ollama compare to OpenRouter?

[Notification Bot]

A message was moved here from #announce > BFS-Prover-V2: A SoTA step-level prover for real use by Patrick Massot.

[George Tsoukalas]

What version of Lean is it trained on?

[Snir Broshi]

Very cool, but why is ByteDance interested in theorem proving?

[(deleted)]

Because theorem proving has many industrial applications

[Zeyu Zheng]

Bas Spitters said:

Looks exciting!
How does LLMLean compare to Lean-LSP-MCP? And how does Ollama compare to OpenRouter?

From what I understand, LLMLean embeds the LLM inside Lean (via tactics like llmstep / llmqed), letting it propose or complete proofs directly. Lean-LSP-MCP treats Lean as a separate logic engine and your agent talks through LSP/MCP interfaces.

[Zeyu Zheng]

Bas Spitters said:

Looks exciting!
How does LLMLean compare to Lean-LSP-MCP? And how does Ollama compare to OpenRouter?

Regarding Ollama vs OpenRouter: Ollama lets you run models locally on your machine. OpenRouter is a unified API gateway to many cloud model providers.

[Zeyu Zheng]

George Tsoukalas said:

What version of Lean is it trained on?

The model was trained on v4.10.0

[(deleted)]

Ancient Lean again. Sad

[Kim Morrison]

I can confirm that the install instructions work, running the LLM locally.

[Kim Morrison]

One thing to note is that while llmstep does print some clickable suggestions in the InfoView, there is not a "blue squiggle" underneath it when the suggestions are ready, so it is easy to miss that it has actually done something.

(This should be fixed!)

[Kim Morrison]

I tried BFS-Prover-V2 on the same example that I had experimented with for reap, i.e. theorem set_smul_closure_subset (as reported by @Yutong Wang in #announce > `reap`: General neural tactic now public available @ 💬 ).

Unfortunately it wasn't particularly successful. The first iteration is good, suggesting refine iUnion₂_subset fun a ha => ?_, but the next step (where reap and Yury used smul_closure_subset), BFS-Prover-V2 just says "No valid suggestions".

[Nicholas Jiang]

Has anyone gotten the planner in the repo working? I've been stuck on verification after the initial generation of the proof sketch. Here's the repo again for reference: https://github.com/ByteDance-Seed/BFS-Prover-V2