Meituan's LongCat team has unveiled LongCat-Flash-Prover, a 560-billion-parameter model designed for mathematical reasoning in Lean4. The model, open-sourced under the MIT license, is available on GitHub, Hugging Face, and ModelScope. It excels in automatic formalization, sketch generation, and full proof generation, achieving a 97.1% pass rate on MiniF2F-Test with 72 reasoning steps. The model employs the Hybrid-Experts Iteration Framework for training and the HisPO algorithm for stable reinforcement learning. It sets new benchmarks in automated formalization and theorem proving, with notable performances on ProverBench and PutnamBench, achieving 70.8% and 41.5% pass rates, respectively.