Lemma is in closed beta
Writing from our R&D teams — findings, methods, and commentary accompanying our published work and products in machine learning, science, and engineering.
How do AI provers handle the messy reality of open-source math? We worked on SorryDB, a community-maintained dynamic benchmark, to measure their performance on real-world Lean formalization projects. Recently presented at ICML.
Our ICML workshop paper introduces Skill-Synthesizer, a query-aware long-term memory system that enables AI agents to synthesize new skills from past experience instead of simply retrieving previous solutions, improving scientific reasoning on challenging physics benchmarks.
We study agentic code generation in Dafny. AxDafny turns code generation into a verifier-guided loop: the model writes Dafny code plus proof annotations, then repairs them using formal verification errors. This work shows large gains in verified correctness, but also a key limitation: proving functional correctness does not guarantee the generated code is efficient.
Our ICML paper introduces AxProverBase, a simple, reproducible, open-source agent that automates theorem proving in Lean — matching far more complex systems while using up to 100× fewer resources.