LongCat-Flash-Prover
Meituan · China
Meituan Lean4 theorem-proving model
- Release month
- Field
- Other
- Availability
- open-weight
- Parameters
- 560B
- License
- mit · Commercial OK
Overview
- Registered on Hugging Face March 20, 2026 · Open weights · 560B
- For Lean4 formalization, proof sketching and proving · 97.1% pass rate on MiniF2F-Test with 72 inferences per problem (company-reported)
View official announcement ↗
← All models