3 papers
cs.AI2026
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
Matěj Kripner, Milan Straka
In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates…
cs.CL2026
Bolzano: Case Studies in LLM-Assisted Mathematical Research
Martin Balko, Jan Grebík, Pavel Hubáček +5
We report new results on eight problems in mathematics and theoretical computer science, produced with the assistance of Bolzano, an open-source multi-agent LLM system. Bolzano orc…
cs.LG2025
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
Matěj Kripner, Michal Šustr, Milan Straka
Automated theorem proving (ATP) has been a classical problem in artificial intelligence since its inception, yet it remains challenging due to its vast state and action space. Larg…