**Website: LeanNotes.wiki** ![[Appendix/Media/Images/Miscellaneous images/Lean Notes Robots.png]] <center><span style="font-size: 1.5em;">The LeanNotes wiki is a budding branch on the Lean knowledge tree.</span></center> <br> <center>The bots worked side-by-side with their favorite smart pets as they built the Lean knowledge tree.</center> <br> <center>The pets are still occasionally referred by their old name, the humans.</center> A Quick look at: - [[LeanNotes Home#LeanNote Sections on Tactics, Proof, and Courses|Sections on Tactics, Proof, and Courses]] - [[LeanNotes GitHub repos]] ## Preface - My name is [[dducoff|Den Ducoff]] and I am a retired math tutor who is studying math, logic, and the Lean language. - I am curating the LeanNotes wiki site as a journal of my lessons, with [[Gemini 3.5]] acting as my tutor. - The LeanNotes wiki pages are organized into the following top level headings: - `Courses and eBooks` : This section includes the Lean learning materials, section by section. - `Proofs`: This section includes the *.lean* proof wiki page annotations. They include the following information: - a list of the tactics used in the proof - the contexts in which the proof is useful - a code block that includes the proof, if it is small - a GitHub link to the *.lean* file that contains the proof - a cross-reference to where these proofs are included in the courses and eBooks - `Tactics` : This section includes the tactics used the proofs. These wiki pages include links to proofs that provide interesting examples of tactic applications. - `Topics` : This section includes the concepts used to explain the LeanNotes methods and resources. These wiki pages include descriptions of: - `AI prompts` : the prompts used to generate LeanNotes content. - [[LeanNotes coding idioms]] : Lean .lean tactic and comment styles that can be useful for non-advanced Lean users. - The [[LeanNotes Zulip channel]] : The repository for community discussions of LeanNotes wiki pages. - Various other topics that clarify important ideas for creating Lean proofs. - **Happy proofing!** ## LeanNote Sections on Tactics, Proof, and Courses ### Tactics - Table of Contents | **`Tactic`** | **`Description`** | | -------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | [apply](app://obsidian.md/apply-tactic) _hypothesis_ | If `hPimpQ : P → Q`is a hypotheses, and the goal is its conclusion type, `⊢ Q`, <br>then invoking `apply hPimpQ` changes the goal from the conclusion <br>to the premise type, `⊢ P`. <br>Once the premise, `P` has been proven, it follows by `Modus Ponens (MP)` <br>that the conclusion, `Q` is proven. | | [apply](app://obsidian.md/apply-at-tactic) _hypotheses_ at _premise_ | If there are hypotheses that assume a conditional and its premise, <br>`hPimpQ : P → Q` and `hP : P`, <br>then `Modus Ponens (MP)` can be applied by invoking <br>**_apply_** `hPimpQ` at `hP`. <br>This will change the type of `hP : P` to the conclusion, `hP : Q`. | ### Propositional Logic - Table of Contents | **`Title`** | **`Logic`** | **`Description`** | | | ------------ | ------------------ | ----------------------------------------- | --- | | [[Identity]] | P → P, ¬P → ¬P | A proposition is equal to itself. | | | [[Negation]] | ¬¬P ↔ P, ¬¬¬P ↔ ¬P | Double negations can be removed in pairs. | | | | | | | ### Theorem Proving in Lean 4 - Avigad, et al. - Table of Contents - **`eBook:`** [Theorem Proving in Lean 4 - Avigad, et al.](https://lean-lang.org/theorem_proving_in_lean4/#) - **`Pdf:`** [[Theorem Proving in Lean 4 - Avigad, et al.pdf]] - **`Solutions Repos:`** [Blacquiere](https://github.com/leanprover-community/tutorials4) [Celsobonutti](https://github.com/celsobonutti/theorem-proving-in-lean-4) [Chabulhwi](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL) [Chun Ding posts: May 20 - June 1, 2025](https://functor.network/user/1/entries) [Ortega](https://github.com/aortega0703/theorem-proving-in-lean-4-solutions/blob/main/chapter-3.lean) #### Solutions - **`2 Dependent Type Theory:`** [Bulhwi Cha](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter02) - **`3 Propositions and Proofs:`** [Bulhwi Cha](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter03) [Celsobonutti](https://github.com/celsobonutti/theorem-proving-in-lean-4/blob/main/TheoremProving/PropositionsAsProofs.lean) [Chun Ding](https://functor.nework/user/1/entry/1094) [Ortega](https://github.com/aortega0703/theorem-proving-in-lean-4-solutions/blob/main/chapter-3.lean) - **`4 Quantifiers and Equality:`** [Bulhwi Cha](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter04) [Celsobonutti](https://github.com/celsobonutti/theorem-proving-in-lean-4/blob/main/TheoremProving/QuantifiersAndEquality.lean) [Chun Ding](https://functor.network/user/1/entry/1100) [Ortega](https://github.com/aortega0703/theorem-proving-in-lean-4-solutions/blob/main/chapter-4.lean) - **`5 Tactics:`** [Bulhwi Cha](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter05) [Chun Ding](https://functor.network/user/1/entry/1119) [Ortega](https://github.com/aortega0703/theorem-proving-in-lean-4-solutions/blob/main/chapter-5.lean) - **`6 Iteracting with Lean:`** [Bulhwi Cha](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Chapter07) - **`7 Inductive Types:`** [Chun Ding](https://functor.network/user/1/entry/1134) - **`8 Induction and Recursion:`** [Chun Ding](https://functor.network/user/1/entry/1137) - **`Exam:`** [Chabulhwi](https://git.sr.ht/~chabulhwi/tpil-solutions/tree/master/item/TPIL/Exam) ## Credits --- **`LeanNotes curator:`** [[dducoff]], [Contact dducoff](https://tally.so/r/rjQYWL) **`Posted Date:`** 2026-08-11