Transform formal proofs into accessible explanations - Making Lean 4 theorems understandable through natural language and beautiful mathematical rendering.
Proof Sketcher bridges the gap between formal verification and human understanding by automatically generating natural language explanations of Lean 4 theorems. Built for researchers, educators, and anyone working with formal mathematics.
🔍 Smart Parsing - Extract theorems and lemmas from Lean 4 files with full AST analysis 📝 Natural Language Generation - Template-based explanations with AI integration roadmap 📊 Modern Export Formats - HTML with MathJax 4.0, Markdown, and batch processing 🎨 Beautiful Rendering - Mathematical notation with professional typesetting 📚 Batch Processing - Handle entire Lean projects with auto-generated indices
- Lean 4 Parser: Complete AST extraction from theorem definitions
- Template Generation: Structured explanations with mathematical context
- Modern HTML Export: Professional output with MathJax 4.0 rendering
- Batch Processing: Handle multiple files with organized output
- Mathematical Notation: Beautiful rendering of Lean expressions
- Auto-Indexing: Generated table of contents and navigation
- AI-Powered Explanations: Claude integration for contextual insights
- Interactive Animations: Dynamic proof visualization with Manim
- PDF Export: LaTeX-quality typesetting for publications
- Doc-gen4 Integration: Seamless mathlib4 documentation workflow
# Clone and install
git clone https://github.com/Bright-L01/proof-sketcher.git
cd proof-sketcher
pip install -e .# Test the complete pipeline
python test_mvp_pipeline.pyfrom proof_sketcher.parser import LeanParser
from proof_sketcher.exporter import HTMLExporter
# Parse Lean file
parser = LeanParser()
theorems = parser.parse_file("my_theorems.lean")
# Generate explanations
exporter = HTMLExporter()
exporter.export_batch(theorems, output_dir="docs/")# Process single file
proof-sketcher explain my_file.lean --output html
# Batch process project
proof-sketcher batch src/ --format html --with-index
# Generate documentation site
proof-sketcher docs src/ --output docs/ --with-nav┌─────────────────┐ ┌─────────────────┐ ┌─────────────────┐
│ Lean 4 AST │───▶│ Template-Based │───▶│ Modern HTML │
│ Parser │ │ Generator │ │ with MathJax │
└─────────────────┘ └─────────────────┘ └─────────────────┘
│ │ │
▼ ▼ ▼
┌─────────────────┐ ┌─────────────────┐ ┌─────────────────┐
│ Theorem AST │ │ Explanation │ │ Professional │
│ Extraction │ │ Templates │ │ Documentation │
└─────────────────┘ └─────────────────┘ └─────────────────┘
- 🔍 Parser Module: Lean 4 file analysis and AST extraction
- 📝 Generator Module: Template-based explanation synthesis
- 🎨 Exporter Module: Multi-format output with professional styling
- 📚 Documentation Engine: Batch processing with organized navigation
- Publication Ready: Generate theorem explanations for academic papers
- Documentation: Create accessible descriptions of formal proofs
- Education: Bridge formal and informal mathematics
- Course Materials: Explain formal proofs to students
- Interactive Learning: Convert Lean theorems to readable content
- Assessment: Document proof understanding and verification
- Mathlib Documentation: Enhanced theorem explanations
- Knowledge Sharing: Make formal proofs more accessible
- Onboarding: Help newcomers understand existing proofs
proof-sketcher/
├── src/proof_sketcher/
│ ├── parser/ # Lean 4 AST extraction
│ ├── generator/ # Explanation generation
│ ├── exporter/ # Multi-format output
│ └── cli.py # Command-line interface
├── tests/ # Comprehensive test suite
├── examples/ # Sample Lean files and outputs
└── docs/ # Documentation and guides
# Development setup
git clone https://github.com/Bright-L01/proof-sketcher.git
cd proof-sketcher
pip install -e ".[dev]"
# Run tests
pytest --cov=proof_sketcher
# Format code
black src/ tests/
ruff check src/ tests/| Feature | Status | Technology |
|---|---|---|
| Lean 4 Parsing | ✅ Complete | Python subprocess, AST analysis |
| Template Generation | ✅ Working | Jinja2, structured templates |
| HTML Export | ✅ Production | MathJax 4.0, responsive CSS |
| Mathematical Rendering | ✅ Professional | LaTeX notation, symbol support |
| Batch Processing | ✅ Efficient | Parallel processing, progress tracking |
| AI Integration | 🚧 Planned | Claude API, contextual enhancement |
| Animation Support | 🚧 Research | Manim integration, dynamic visualization |
- First of its kind: Dedicated Lean 4 to natural language tool
- Modern Technology: Built with latest web standards and rendering
- Research Foundation: Grounded in formal verification best practices
- Extensible Design: Modular architecture for future enhancements
- AST-Level Analysis: Deep understanding of theorem structure
- Template-Based Generation: Consistent, reliable explanations
- Professional Output: Publication-quality mathematical rendering
- Scalable Processing: Handle large Lean projects efficiently
- API Reference - Complete function documentation
- User Guide - Step-by-step tutorials
- Architecture - Technical design details
- Contributing - Development guidelines
- Examples - Sample inputs and outputs
- GitHub Issues: Bug reports and feature requests
- Discussions: Community Q&A and ideas
- Contributing: Welcome contributions from the Lean community
- Academic Collaboration: Open to research partnerships
MIT License - See LICENSE for details.
Making formal mathematics accessible, one proof at a time. 🎓
Contact • Issues • Discussions