Pantograph / PyPantograph

A programmatic Lean interface for proof search, reasoning experiments and proof-state interaction.

• Developer / Organization: Stanford CENTAUR / Pantograph contributors
• Category: Open-source skills & interfaces
• Purpose: Provide machine-to-machine access to Lean proof states.
• Key features: A programmatic Lean 4 interface for implementing proof search and agent workflows.
• Availability: Open-source software; Apache-2.0
• License: Apache-2.0 (source (opens in a new tab))
• Website / Source code: https://github.com/stanford-centaur/PyPantograph (opens in a new tab)
• Version: GitHub release v0.3.15
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01