Lean4

Learning materials and exercises for theorem proving and formal logic using the Lean 4 proof assistant.

Overview

This repository contains coursework and exercises focused on:

• Propositional logic and natural deduction
• Formal proof construction in Lean 4
• First-order logic reasoning
• Mathematical theorem proving

Contents

Core Learning Files

• lean_inference_rules.md - Comprehensive reference table of inference rules in Lean 4, covering:

  • Implication (→-Intro, →-Elim, Modus Tollens)
  • Conjunction (∧-Intro, ∧-Elim)
  • Disjunction (∨-Intro, ∨-Elim)
  • Negation (¬-Intro, ¬-Elim)
  • Biconditional (↔-Intro, ↔-Elim)
  • Universal quantification (∀-Intro, ∀-Elim)
  • Existential quantification (∃-Intro, ∃-Elim)
  • Each rule shown in both term mode and tactic mode

• lean_inference_rules_printable.pdf - Printable reference card for inference rules

Assessment Files

• assessment1.lean - Main assessment file working with axioms and proof construction

  • Custom axioms for conjunction operations
  • Proofs involving provable predicates
  • Exercises on contradiction, conjunction rearrangement, and negation

• assessment.experiments.lean - Experimental work related to assessments

Unit-Based Exercises

• unit3.l1.lean - Unit 3, Lesson 1 exercises
• unit3.l2.lean - Unit 3, Lesson 2 exercises
• unit3.l3.lean - Unit 3, Lesson 3 main content
• unit3.l3.examples.lean - Examples for Unit 3, Lesson 3
• unit3.l3.formative.lean - Formative assessment for Unit 3, Lesson 3
• unit3.l5.lean - Unit 3, Lesson 5 exercises
• unit5.l5.formative.lean - Formative assessment for Unit 5, Lesson 5

Additional Resources

• examples.lean - Real-world AI and decision scenario examples translated into propositional logic
• additionalGuidance.lean - Extra guidance on proof techniques
• learningfp.lean - Functional programming concepts in Lean
• simpleleanproof.lean - Basic proof examples
• universalAndExistential.lean - Quantifier exercises

Other Files

• tarski.jar - Tarski's World application for logic visualization (Java)

Key Concepts Covered

Natural Deduction

The exercises focus on constructing proofs using natural deduction rules in Lean 4. Both term mode (direct proof construction) and tactic mode (interactive proof construction) are used throughout.

Custom Axioms

Several files work with custom axiom systems, such as:

opaque conj : Prop -> Prop -> Prop
opaque provable : Prop -> Prop

axiom AxConjElimRight : ∀ x y, provable (conj x y) -> provable y
axiom AxConjElimLeft : ∀ x y, provable (conj x y) -> provable x
axiom AxConjIntro : ∀ x y, provable x -> provable y -> provable (conj x y)

These axioms define custom logical operators and their elimination/introduction rules.

Proof Techniques

• Implication introduction and elimination (Modus Ponens, Modus Tollens)
• Conjunction (introduction and both elimination rules)
• Disjunction (case analysis)
• Negation (proof by contradiction)
• Ex Falso Quodlibet (from contradiction, anything follows)
• Universal and existential quantification

Learning Approach

The materials progress through:

1. Basic propositional logic (implication, conjunction, disjunction)
2. Negation and contradiction
3. Natural deduction inference rules
4. First-order logic with quantifiers
5. Real-world scenario modeling in formal logic
6. Custom axiom systems and abstract reasoning

Technologies

• Lean 4 - Theorem prover and proof assistant
• Natural Deduction - Proof methodology
• First-Order Logic - Logical framework

Getting Started with Lean 4

To work with these files:

1. Install Lean 4 from https://leanprover.github.io/
2. Install a Lean 4-compatible editor (VS Code with Lean 4 extension recommended)
3. Open any .lean file to see proofs and exercises
4. Replace sorry placeholders with actual proofs

Example Proof Structure

-- Term mode
theorem example1 (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q :=
  And.intro hp hq

-- Tactic mode
theorem example2 (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by
  exact And.intro hp hq

Real-World Applications

The examples.lean file demonstrates translating real-world scenarios into formal logic, such as:

• Student grant eligibility based on competition wins or publications
• Verification by supervisors or committees
• Decision-making under multiple conditions

Further Reading

• Lean 4 Documentation
• Theorem Proving in Lean 4
• Natural Deduction
• First-Order Logic