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
  • A Z3-style Symbolic Reasoning API for Python, backed by Lean 4
    • Boolean Logic
    • Solvers
    • Arithmetic
    • Satisfiability and Validity
    • Machine Arithmetic
    • Functions
    • Uninterpreted Sorts
    • Quantifiers
    • Arrays
    • Sets
    • Algebraic Datatypes
      • Enumerations
      • Records
      • Recursive Datatypes
      • Recognisers
      • DatatypeSortRef API
      • Convenience Constructors
    • Strings
    • Regular Expressions
    • Floating Point
    • Pseudo-Boolean Constraints
    • Characters and Finite Domains
    • Tactics and Goals
      • Tactic Combinators
      • Arbitrary Lean Tactics
      • Available Tactics
      • Probes
      • The Simplifier
    • SMT-LIB2 Parsing
    • Fixedpoint (Datalog)
    • List Comprehensions
    • Substitution and Lambdas
    • Puzzles
      • Eight Queens
      • Dog, Cat, and Mouse
    • Expression Introspection
    • Serialisation
    • Advanced Setup
    • What Works
    • Comparison with z3py

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.