High-impact Topics
Automated theorem proving, scientific discovery agents, multimodal symbolic reasoning, program synthesis and verification.
CCF Big Data & Computing Intelligence Contest Formal Math Competition for LLMs
An innovation challenge for LLMs, advancing verifiable formal mathematics reasoning.
Why Join
Advance verifiable and controllable AI, compete with top teams, and produce reproducible, auditable research and systems.
Systematic Evaluation
Measure correctness, robustness, and traceability; emphasize end-to-end workflows and standardized artifacts.
Attractive Incentives
Grand champion, track champions, and special awards; opportunities for showcasing and collaboration.
Tracks
Automated Theorem Proving
Model-guided strategies and toolchain co-design.
Scientific Discovery Agents
End-to-end agents from literature to experiment.
Multimodal Symbolic Reasoning
Verified reasoning across text, charts, and equations.
Key Dates
- 10-20
- 10-20 to 10-30
Practice
- 11-03 to 11-28
Preliminary
- 12-04 to 12-05
Final
- 12-31
End
Organizers & Support
Hosted by CCF, co-organized by industry and academia for the future of Formal Methods × AI.
Contact
For partnership/media/sponsorship, see the organizers page or email us.
FAQ Highlights
Do I need to open source?
Finalist teams must provide reproducible artifacts. Terms to be finalized.
Can I join multiple tracks?
Yes. Submit separately per track and follow the rules.
Ready?
Register now, get guides and baselines, and start your verifiable AI journey.