open-atp prove Lemma.lean result/ claude
I took a class on formal verification back in 2022 when I was an undergraduate. There was something incredibly satisfying about constructing proofs in Coq and knowing my statements were now formally verified. However, formal methods were so time consuming that they weren't practical in most industry settings. The rise of AI has changed that story: https://blog.janestreet.com/formal-methods-at-jane-street-in....
AI is producing algorithms and mathematical proofs far faster than humans can review them and formal methods offer a solution. Automated theorem provers take a statement formalized in a proof assistant like Lean and attempt to supply a proof. Unlike natural language proofs, these proofs can be machine-checked, reducing the burden of review on humans.
AI agents are powerful automated theorem provers. Even general purpose coding agents, like Claude Code, can be effective provers with the right skills and tooling. However, these methods are currently challenging to run. They require configuring Docker containers with the proper Lean environment and agent tooling (skills, plugins, MCP, credentials). Furthermore, there is not a common interface to existing provers.
OpenATP aims to solve both of these challenges! It makes it easy to run methods locally in Docker or remotely in Modal. It currently supports the following provers: https://open-atp.henryrobbins.com/en/latest/provers/index.ht....