Show HN: OpenATP: A platform for automated theorem proving in Lean
By henryrobbins00 · 2026-06-30 · 3 points · 0 comments
https://github.com/henryrobbins/open-atp
TL;DR: I created a Python package to make running agentic automated theorem provers (e.g., Aristotle, Numina-Lean-Agent, Claude Code, etc...) as simple as open-atp prove Lemma.lean result/ claude I took a class on formal verification back in 2022 when I was an undergraduate…
Open the full discussion on BetterNews