AI discovers formally verified quantum programs
LLM agents synthesize novel quantum programs in Lean and verify them, improving baselines by up to 290x.
Stories per day · 30 days
2 RSS
Relatedlean3formal-verification2aegis1agents1easyprover1formal-methods1graph-search1llm-agents1mathlib1quantum-computing1retrieval1rust1test-time-compute1
6 stories, newest first · one card per story
Stories tagged #theorem-proving
EasyProver solves near-saturated Lean benchmarks and half of harder Aegis tasks
On a stratified Aegis sample of 2,000 statements, it proves 1,054 within a 30-minute budget.
Simple Lean 4 harness h1 matches specialized prover workflows
With matched models, a single attempt plus verifier feedback solved eight open FormalConjectures problems and led three formal benchmarks.
Lean Graph Search for Formal Theorem Proving
LeanGraphSearch retrieves supporting Lean lemmas via dependency graphs and lifts theorem-proving pass rates.
Learning to Discover Interesting Mathematics
A 27B model ranks mathematical theorems by interestingness and cuts Mathlib overlap from 91.9% to 30.6%.
Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science
Stellar Colosseum, a many-agent harness for long-horizon math and TCS research, solves open problems and reaches 71% on TCS-Bench with Gemini models.