Formal Conjectures: A Formal Math Benchmark
blaiseaguera · x · 2026-07-14
The author announces a collaboration with Google DeepMind to launch Formal Conjectures, an evolving Lean 4 benchmark designed to evaluate AI's formal mathematical capabilities.
Core Features
- Utilizes 1,029 open conjectures as a "zero-contamination" reasoning test set to minimize training data leakage.
- Provides an additional 836 solved problems for auto-formalization tasks.
- Requires kernel-level correctness, ensuring that final proofs strictly hold up at the Lean kernel level.
The author adds that this work is already facilitating new discoveries and forging closer ties between the formal math community and automated solvers. The open-source code has also been released.
More from Research
- FrontierCS 2 launches on Kaggle: 48 tasks make agents beat published CS papers — MeganRisdal · 2026-10-27
- LightMTP: lightweight latent multi-token prediction boosts LLM planning in pretraining — gdm3000 · 2026-10-27
- DexPort: a handheld interface with a real robot hand for dexterous-hand data collection — pabbeel · 2026-10-27
- EMNLP study: AI literary translation reads fine but varies more, even within one book — tuvllms · 2026-10-27
- Lab monkeys at $30-80K each: a 4-year breeding cycle is the real preclinical drug bottleneck — zebird0 · 2026-10-27
- Custom VQA benchmark under 48GB VRAM: Qwen3.8-Flash-Next leads, Qwen3.8-27B regressed — EmilPi · 2026-10-27