Add LeanNotebook: Interactive Tutorial System for Learning Lean and Physical Mathematics

[Copilot]

Overview

This PR implements a comprehensive LeanNotebook tutorial system that provides interactive, guided learning resources for exploring pure functions, λ-calculus, and physical mathematics concepts using the Lean 4 theorem prover.

What's New

📚 Four Progressive Tutorial Notebooks

1. Introduction.lean (~30 min, Beginner)

• First steps in Lean theorem proving
• Simple function definitions and examples
• Basic proof techniques using reflexivity
• Introduction to the PhysicalMathematics library

2. PureFunctions.lean (~45 min, Beginner-Intermediate)

• Deep dive into pure functions and their properties
• Referential transparency and function composition
• Working examples with factorial and fibonacci
• Formal proofs demonstrating function consistency

3. LambdaCalculus.lean (~60 min, Intermediate)

• λ-calculus foundations and theory
• Church numerals: encoding numbers as functions
• Church arithmetic operations
• SKI combinator calculus demonstrating universal computation
• β-reduction and stateless computation principles

4. QuantumMathematics.lean (~60 min, Intermediate-Advanced)

• Mathematical consistency and Gödel's incompleteness theorems
• Riemann zeta function approximations
• Quantum groups and symmetry theory
• Hilbert spaces and quantum state modeling
• Observable quantities, measurements, and entanglement

📖 Comprehensive Documentation Suite

For Getting Started:

• QUICKSTART.md - Complete setup guide with installation, troubleshooting, and first steps
• LeanNotebook/START_HERE.md - Friendly entry point with 3 curated learning paths and progress tracking

For Reference:

• LeanNotebook/CHEATSHEET.md - Complete Lean 4 syntax reference with examples covering functions, types, theorems, tactics, and common patterns
• LeanNotebook/OVERVIEW.md - Detailed content breakdown for each notebook with learning paths, skill development, and tips
• LeanNotebook/FILE_GUIDE.md - Navigation guide helping users find content based on their needs
• LeanNotebook/README.md - Comprehensive guide to using the notebooks with prerequisites and structure

🔧 Project Integration

• Updated lakefile.lean to include the new LeanNotebook library
• Created LeanNotebook.lean module that imports all tutorial notebooks
• Enhanced main README.md with notebook documentation and quick start link

Learning Paths

Users can choose from three distinct paths based on their goals:

1. Beginner Path (~2 hours) - Focus on basics and pure functions
2. Complete Tour (~3-4 hours) - Comprehensive exploration of all concepts
3. Physical Mathematics Focus (~2.5 hours) - Emphasizes connections between mathematics and quantum physics

Content Highlights

The notebooks demonstrate practical concepts including:

• Church numerals and Church arithmetic
• SKI combinator calculus
• Riemann zeta function approximations
• Quantum state modeling and entanglement
• Formal proofs about factorial and fibonacci functions
• Group theory and symmetries
• Logic gates (classical and quantum)

Alignment with Project Goals

This implementation directly supports the themes mentioned in the project README:

• ✅ Pure functions and their properties
• ✅ λ-calculus fundamentals and statelessness
• ✅ Mathematical consistency
• ✅ Quantum groups (from References section)
• ✅ Riemann zeta function (Terence Tao's work)
• ✅ Logic gates (熱門)

Technical Details

• 600+ lines of well-documented Lean 4 code
• 1,500+ lines of supporting documentation
• 11 new files organized in a clear structure
• All notebooks include extensive inline comments and explanations
• Examples are runnable and testable in VS Code with the Lean 4 extension

Usage

Users can get started by:

1. Reading QUICKSTART.md for setup instructions
2. Opening LeanNotebook/START_HERE.md to choose a learning path
3. Working through notebooks interactively in VS Code
4. Referring to CHEATSHEET.md for syntax help as needed

The notebooks are designed for progressive learning, with each building on concepts from the previous one while remaining accessible to newcomers to Lean and formal mathematics.

Benefits

• Lowers the barrier to entry for learning Lean 4
• Provides practical, hands-on examples of theorem proving
• Connects abstract mathematical concepts to physical applications
• Offers multiple learning paths for different audiences
• Includes comprehensive reference materials for self-directed learning

Closes #[issue_number]

Original prompt

---

This section details on the original issue you should resolve

<issue_title>LeanNotebook</issue_title>
<issue_description></issue_description>

Comments on the Issue (you are @copilot in this section)

Fixes #7

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.