collaborators

1 paper

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…