Python to Lean4 Translator

Translate Python programs into equivalent, executable Lean4 code while preserving program semantics and ensuring type safety.

Overview

This skill provides systematic guidance for translating Python code to Lean4, handling type inference, function translations, data structures, control flow, and ensuring well-typed, executable output.

Translation Workflow

Python Input → Analyze Structure → Map Types → Translate Constructs → Verify → Output Lean4
    ├─ Identify types and signatures
    ├─ Map Python constructs to Lean4 equivalents
    ├─ Handle type conversions
    ├─ Ensure totality and termination
    └─ Validate executability

Core Translation Principles

1. Type Safety First

Lean4 is strongly typed. Every translation must:

• Infer or specify explicit types for all variables
• Ensure type consistency across operations
• Handle Python's dynamic typing by choosing appropriate Lean4 types
• Use

  Option

  for nullable values,

  Except

  for error handling

2. Preserve Semantics

The translated code must maintain the same computational behavior, preserve function input-output relationships, keep the same algorithmic complexity, and handle edge cases equivalently.

3. Ensure Executability

Generated Lean4 code must compile without errors, be executable (use

#eval

Type Mapping Reference

Basic Types

int

Int

Nat

Nat

float

Float

bool

Bool

str

String

None

Option α

none

some x

list

List α

tuple

α × β

dict

Std.HashMap

List (α × β)

set

Std.HashSet

List α

For detailed type system information, see references/type_mappings.md.

Translation Patterns

Functions

Simple function:

def add(a: int, b: int) -> int:
    return a + b

Lean4:

def add (a : Int) (b : Int) : Int :=
  a + b

Recursive function:

def factorial(n: int) -> int:
    if n <= 1:
        return 1
    else:
        return n * factorial(n - 1)

Lean4:

def factorial (n : Nat) : Nat :=
  if n ≤ 1 then
    1
  else
    n * factorial (n - 1)

Control Flow

If-else:

if condition:
    result = value1
else:
    result = value2

Lean4:

let result := if condition then value1 else value2

For loops (list iteration):

total = 0
for x in items:
    total += x

Lean4 (using fold):

let total := items.foldl (· + ·) 0

List Operations

List comprehension:

squares = [x * x for x in range(10)]

Lean4:

let squares := (List.range 10).map (fun x => x * x)

Filter:

evens = [x for x in numbers if x % 2 == 0]

Lean4:

let evens := numbers.filter (fun x => x % 2 == 0)

Classes and Structures

Python class:

class Rectangle:
    def __init__(self, width: int, height: int):
        self.width = width
        self.height = height

    def area(self) -> int:
        return self.width * self.height

Lean4:

structure Rectangle where
  width : Int
  height : Int

def Rectangle.area (r : Rectangle) : Int :=
  r.width * r.height

Handling Common Challenges

1. Dynamic Typing

Analyze usage to infer types, use sum types for multiple possible types, use

Option

2. Mutability

Use immutable bindings with

let

StateM

3. Exceptions

Convert Python exceptions to

Except

Option

def divide(a: int, b: int) -> float:
    if b == 0:
        raise ValueError("Division by zero")
    return a / b

Lean4:

def divide (a b : Int) : Except String Float :=
  if b = 0 then
    Except.error "Division by zero"
  else
    Except.ok (a.toFloat / b.toFloat)

4. Recursion and Termination

Use structural recursion when possible, add

termination_by

def fibonacci (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fibonacci n + fibonacci (n + 1)
termination_by n

5. Side Effects and I/O

Use

IO

def greet(name: str):
    print(f"Hello, {name}!")

Lean4:

def greet (name : String) : IO Unit :=
  IO.println s!"Hello, {name}!"

Translation Process

Step 1: Analyze Python Code

Identify all functions, classes, and global variables. Infer types from usage and annotations. Identify dependencies and imports. Note any dynamic behavior or side effects.

Step 2: Plan Type Mappings

Map Python types to Lean4 types. Identify where

Option

Except

Step 3: Translate Constructs

Start with data structures (classes → structures). Translate pure functions first. Handle control flow (convert loops to recursion). Translate functions with side effects using

IO

Step 4: Ensure Well-Typedness

Add explicit type annotations. Resolve type mismatches. Handle implicit conversions. Add termination proofs for recursive functions.

Step 5: Verify Executability

Check syntax with Lean4 compiler. Test with

#eval

Required Imports

Common imports for translated code:

import Std.Data.HashMap
import Std.Data.HashSet
import Init.Data.List.Basic
import Init.Data.Option.Basic

Example Translation

Python:

def is_prime(n: int) -> bool:
    if n < 2:
        return False
    for i in range(2, int(n ** 0.5) + 1):
        if n % i == 0:
            return False
    return True

def primes_up_to(limit: int) -> list[int]:
    return [n for n in range(2, limit + 1) if is_prime(n)]

Lean4:

def isPrime (n : Nat) : Bool :=
  if n < 2 then
    false
  else
    let rec checkDivisors (i : Nat) : Bool :=
      if i * i > n then
        true
      else if n % i = 0 then
        false
      else
        checkDivisors (i + 1)
    checkDivisors 2

def primesUpTo (limit : Nat) : List Nat :=
  (List.range (limit + 1)).drop 2 |>.filter isPrime

-- Test
#eval primesUpTo 20  -- [2, 3, 5, 7, 11, 13, 17, 19]

Best Practices

1. Start Simple: Translate simple functions first, then build up to complex ones
2. Test Incrementally: Use

   #eval

   to test each function as you translate
3. Document Assumptions: Note any assumptions about types or behavior
4. Preserve Structure: Keep similar code organization when possible
5. Use Lean4 Idioms: Prefer pattern matching over if-else chains
6. Handle Errors Explicitly: Use

   Option

   or

   Except

   instead of exceptions
7. Prove Termination: Add termination proofs for recursive functions
8. Comment Differences: Note where Lean4 behavior differs from Python

Verification Checklist

Before finalizing translation:

• All types are explicitly specified or correctly inferred
• Code compiles without errors

• #eval

  produces expected results for test cases
• Recursive functions have termination proofs
• Error handling uses

  Option

  or

  Except

  appropriately
• Side effects are properly wrapped in

  IO

• Imports are included
• Comments explain non-obvious translations

Additional Resources

For complex translations, refer to:

• Type Mappings - Comprehensive type conversion guide
• Common Patterns - Frequently used translation patterns
• Advanced Features - Monads, type classes, and advanced Lean4 features