Lean First Steps

Code for "Lean First Steps" course.

You should be able to download this repository and "Open Folder" in VSC.

As long as VSC has the Lean4 extension, the correct lean environment will be created automatically.

Name		Name	Last commit message	Last commit date
Latest commit History 177 Commits
slides		slides
.gitignore		.gitignore
00_scratch.lean		00_scratch.lean
01_first_proof.lean		01_first_proof.lean
02_simple_calc.lean		02_simple_calc.lean
03_symbolic.lean		03_symbolic.lean
04_algebra.lean		04_algebra.lean
05_inequality.lean		05_inequality.lean
06_intermediate_result.lean		06_intermediate_result.lean
07_proof_by_cases.lean		07_proof_by_cases.lean
08_conjunctive_hypothesis.lean		08_conjunctive_hypothesis.lean
09_disjunctive_goal.lean		09_disjunctive_goal.lean
10_conjunctive_goal.lean		10_conjunctive_goal.lean
11_existence.lean		11_existence.lean
12_definition_odd_number.lean		12_definition_odd_number.lean
13_lemma_ne_of_lt.lean		13_lemma_ne_of_lt.lean
14_lemma_ne_of_lt_at_h.lean		14_lemma_ne_of_lt_at_h.lean
15_mul_eq_zero.lean		15_mul_eq_zero.lean
16_writing_our_own_lemma.lean		16_writing_our_own_lemma.lean
17_using_our_lemma.lean		17_using_our_lemma.lean
18_our_own_definition.lean		18_our_own_definition.lean
19_proof_by_contradiction.lean		19_proof_by_contradiction.lean
20_contradictory_case.lean		20_contradictory_case.lean
21_induction.lean		21_induction.lean
22_recursion.lean		22_recursion.lean
LICENSE		LICENSE
LeanFirstSteps.lean		LeanFirstSteps.lean
README.md		README.md
exercise_solutions.lean		exercise_solutions.lean
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain

Provide feedback