One model DeepSeek-Prover achieves new state-of-the-art results in theorem proving, leveraging large-scale synthetic data to outperform GPT-4 on benchmarks like miniF2F and FIMO. Available for research and commercial use.