evo-lean-induction-proof

Lean 4 Induction Proof Skill

Overview

This skill handles Lean 4 proof completion tasks where:

• A recursive sequence is defined (e.g., partial sums of a geometric series)
• A bound must be proved for all natural numbers
• The proof environment uses Heather Macbeth's Math2001 library tactics

Key Proof Strategy

Stronger Helper Lemma Pattern: When proving S n ≤ bound for a recursive sequence, direct induction often fails because the inductive hypothesis S k ≤ bound is too weak. Instead:

1. Find the closed-form expression for S n (e.g., S n = 2 - 1/2^n)
2. Prove S m = closed_form by simple_induction
3. Rewrite the goal with the closed form
4. Prove the bound using positivity of the remainder term

Tactic Reference (Math2001 library):

• simple_induction n with k IH — standard induction with push_cast
• simp [S] — unfold the recursive definition
• rw [IH] — apply induction hypothesis
• rw [pow_succ] — rewrite 2^(k+1) as 2^k * 2
• ring — close algebraic goals over commutative rings
• norm_num — numeric normalization
• linarith — linear arithmetic
• addarith — weaker linear arithmetic (from library)
• positivity — prove positivity goals (from Mathlib)
• div_pos, pow_pos — positivity lemmas for division and powers

Compilation:

• Use lake env lean solution.lean (not lean directly, not lake build)
• No output = success; any output indicates errors or warnings
• Warnings must be treated as errors (remove unused variables)
• Avoid field_simp — may not be available in all configurations

Usage

import sys
sys.path.insert(0, '/app/environment/skills/evo-lean-induction-proof/scripts')
from utils import run_end_to_end, validate_solution, read_template, get_prefix_lines, write_solution, compile_lean

# End-to-end: reads template, generates proof, writes, compiles, validates
result = run_end_to_end(
    workspace_dir='/app/workspace',
    solution_file='solution.lean',
    proof_start_line=15,  # line where proof body starts
    timeout=300
)
print(f"Success: {result['success']}")
if not result['success']:
    print(f"Issues: {result['issues']}")

# Validation only (after manual proof writing)
lines = read_template('/app/workspace/solution.lean')
prefix = get_prefix_lines(lines, 15)
val = validate_solution('/app/workspace', 'solution.lean', prefix, 15)
print(f"Valid: {val['valid']}, Issues: {val['issues']}")