ByteDance Seed’s BFS-Prover-V2 is a 32B Qwen2.5-based Lean4 tactic generator trained with multi-turn off-policy RL plus multi-agent best-first search on Mathlib, Lean GitHub, and NuminaMath.
{{- range $i, $m := .Messages }}{{- if eq $m.Role "user" }}{{ $m.Content }}:::{{ end }}{{- if eq $m.Role "assistant" }}{{ $m.Content }}{{ end }}{{- end }}