lean-py

Getting Started

  • Getting Started
    • Prerequisites
    • Installation
    • Quick Start
    • Pattern Matching (Python 3.10+)
    • Calling Python from Lean
    • Kernel Facade
    • Exception Handling
    • Next Steps
  • Setting Up a Project
    • Directory Layout
    • Step 1: Create the Lean Project
    • Step 2: Write Lean Code
    • Step 3: Build
    • Step 4: Create the Python Project
    • Step 5: Call Lean from Python
    • Using Additional Lake Dependencies
    • Type Marshalling Reference
    • Pattern Matching on Inductives

Examples

  • Basic Example
    • The Lean side
      • Exporting a function
      • Exporting a structure
      • Exporting an inductive
      • Making it all visible
    • The Python side
    • Running it
    • What to take away
  • Pantograph Kernel
    • Setting up
    • Loading an environment
    • Introspecting declarations
    • Running the elaborator
    • Creating goals and running tactics
    • Frontend processing
    • Goal state lifecycle
    • What to take away
  • Typed NumPy
    • The idea
    • Calling into Python
    • Reshape with proof obligations
    • A demo pipeline
    • Running it
    • What to take away
  • SymPy Tactic
    • The architecture
    • The oracle axiom
    • The Lean tactic
    • Converting Expr to SymPy
    • Using the tactic
    • Running
    • What to take away
  • Z3 / Knuckledragger Tactic
    • Same architecture, different solver
    • Converting Expr to Z3
    • Checking with Knuckledragger
    • Using the tactic
    • Running
    • Comparing SymPy and Z3
    • What to take away
  • Effectful Refinement-Type Verifier
    • The idea
    • The Lean side
    • Refinement annotations
    • Symbolic execution with effectful
    • Building Lean.Expr trees
      • De Bruijn indices
      • Converting Terms to Exprs with handlers
    • Verification via omega
    • The demo
    • What to take away

API Reference

  • Library Loading
    • Loading from a Lake project
      • Loading from a path
    • What happens at load time
    • Calling functions
    • Working with types
    • API reference
  • Kernel
    • Setup
    • Loading an environment
    • Querying declarations
    • Elaboration
    • Creating goals and running tactics
      • Prograde tactics
      • Conv and calc modes
    • Goal state lifecycle
    • Environment serialisation
    • Frontend processing
    • API reference
      • Kernel
      • GoalState
      • TacticResult
  • Marshalling
    • How values cross the boundary
      • Scalar types
      • Container types
      • Inductive types
    • LeanObj — owned pointers
    • LeanInductiveValue — Python-side inductives
    • Smart constructors
    • The Marshaller class
    • API reference
  • Registry
    • Where the data comes from
    • TypeRepr — describing Lean types
    • CtorInfo — constructor metadata
    • TypeInfo — type metadata
    • FuncInfo — function metadata
    • LibraryRegistry — the full picture
    • API reference
  • Exceptions
    • LeanError
    • LeanPyCallbackError
    • API reference
lean-py
  • Search

© Copyright 2025, Kiran Gopinathan.

Built with Sphinx using a theme provided by Read the Docs.