Show HN: OpenATP: A platform for automated theorem proving in Lean

Category: devtools

Tags: automated-theorem-proving, lean, ai-agents

Score: 7.0/10 (Innovation: 7, Technical: 7, Documentation: 8, Utility: 6)

OpenATP is a Python package that provides a unified interface for automated theorem proving in Lean, supporting multiple agentic provers in isolated Docker sandboxes. It combines recent AI-driven proof methods with benchmarking utilities, making advanced theorem proving more accessible and reproducible.

Target audience: backend devs, data engineers, researchers

Repository: https://github.com/henryrobbins/open-atp · Python · MIT · 1 stars

View on Hacker News