Individual skill

evo-lean4-recursive-sequence-inequality-proof

Provides utilities and guidance for constructing Lean 4 proofs involving recursive sequences and geometric sum inequalities. Covers reading existing Lean template files, crafting induction-based proofs with closed-form intermediate lemmas, and using math2001 textbook tactics (simple_induction, numbers, addarith, extra, rel) plus Mathlib4 tactics (norm_num, linarith, positivity, ring, field_simp) to handle arithmetic over rationals with powers of 2.

tasks-evolved/lean4-proof/environment/skills/evo-lean4-recursive-sequence-inequality-proof/SKILL.md

Read pinned source

Source commit 84ca182da055fafb6453dcec4a6defdbbfd987c1

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: No
Repository scan complete: No
Skill scan complete: No
Observed behavior: Not checked yet
Last checked: Nov 6, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 98
Repository last updated: Sep 10, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

agent-skills Repository topic
ai-agents Repository topic
llm-agents Repository topic
open-world Repository topic
self-evolving-agents Repository topic
engineering Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 4,076 bytes
SKILL.mdcore · 4,076 bytes
scripts/utils.pyruns · 2,945 bytes

Read excerpt


# Lean 4 Recursive Sequence Inequality Proof Skill

## Overview

This skill solves problems of the form: given a recursively defined sequence
`S : ℕ → ℚ` (e.g., geometric partial sums), prove an inequality like `S n ≤ C`
for all natural numbers.

## Key Strategy: Closed-Form Lemma + Inequality

The recommended proof approach has two parts:

1. **Prove a closed-form lemma**: Show `S n = 2 - 1 / 2^n` by induction
2. **Derive the inequality**: Since `1/2^n ≥ 0`, we get `S n = 2 - 1/2^n ≤ 2`