Lean 4 Lessons

Centralized repository of curated lessons learned from formal verification projects in Lean 4. Includes keyword search, semantic search (embeddings), contradiction detection, and a relationship graph.

Structure

lean4/                          # Lesson markdown files (source of truth)
├── tacticas.md                 # Tactics and proof patterns
├── arquitectura.md             # Proof architecture and bridge lemmas
├── campos-finitos.md           # Finite fields and ZMod
├── induccion.md                # Induction and recursion patterns
├── anti-patrones.md            # Anti-patterns to avoid
├── vr1cs-unionfind.md          # Union-Find, EGraph, array reasoning
├── qa-workflow.md              # QA workflows and expert consultation
└── INDEX.md                    # Master quick-reference table
scripts/
├── query_lessons.py            # Query interface (keyword, semantic, hybrid)
├── save_lessons.py             # Save new lessons with auto-classification
├── build_lessons_index.py      # Rebuild index + embeddings from .md files
└── semantic.py                 # Semantic layer (PEP 723, run via uv)

Setup

Requires Python 3.10+ and uv for semantic features.

# Build index and embeddings (first time after clone)
python3 scripts/build_lessons_index.py --verbose

This generates lean4/lessons_index.json (keyword index + relationship graph) and lean4/lessons_embeddings.npz (semantic embeddings via BAAI/bge-small-en-v1.5). Both are .gitignored as generated artifacts.

Usage

# Exact lesson lookup
python3 scripts/query_lessons.py --lesson L-153

# Keyword search
python3 scripts/query_lessons.py --search "omega multiplication"

# Semantic search (natural language)
python3 scripts/query_lessons.py --semantic "how to handle nonlinear arithmetic"

# Hybrid search (keyword + semantic, recommended)
python3 scripts/query_lessons.py --hybrid "omega no puede conmutar multiplicación"

# Problem lookup
python3 scripts/query_lessons.py --problem "omega no funciona"

# Related lessons (graph)
python3 scripts/query_lessons.py --related L-153

# Save new lessons (from JSON)
echo '[{"title":"...","body":"...","keywords":["kw1"]}]' | python3 scripts/save_lessons.py

Semantic layer

semantic.py is a self-contained PEP 723 script — dependencies are declared inline and managed by uv. No manual pip install needed. On first run, uv downloads fastembed (~50MB) and the embedding model (~30MB) to its cache.

Contradiction detection runs automatically when saving lessons: if a new lesson is >82% similar to an existing one, a warning is emitted.