|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
####### # # E-scripts on the Lean theorem prover / proof assistant. # # Note 1: use the eev command (defined in eev.el) and the # ee alias (in my .zshrc) to execute parts of this file. # Executing this file as a whole makes no sense. # An introduction to eev can be found here: # # (find-eev-quick-intro) # http://angg.twu.net/eev-intros/find-eev-quick-intro.html # # Note 2: be VERY careful and make sure you understand what # you're doing. # # Note 3: If you use a shell other than zsh things like |& # and the for loops may not work. # # Note 4: I always run as root. # # Note 5: some parts are too old and don't work anymore. Some # never worked. # # Note 6: the definitions for the find-xxxfile commands are on my # .emacs. # # Note 7: if you see a strange command check my .zshrc -- it may # be defined there as a function or an alias. # # Note 8: the sections without dates are always older than the # sections with dates. # # This file is at <http://angg.twu.net/e/lean.e> # or at <http://angg.twu.net/e/lean.e.html>. # See also <http://angg.twu.net/emacs.html>, # <http://angg.twu.net/.emacs[.html]>, # <http://angg.twu.net/.zshrc[.html]>, # <http://angg.twu.net/escripts.html>, # and <http://angg.twu.net/>. # ####### # «.regular-install-2021» (to "regular-install-2021") # «.lean-3.4.2» (to "lean-3.4.2") # «.vscode» (to "vscode") # «.delete-lean» (to "delete-lean") # «.lean-mode» (to "lean-mode") # «.topos» (to "topos") # «.diagram-chasing» (to "diagram-chasing") # «.theorem_proving_in_lean» (to "theorem_proving_in_lean") # «.natural-number-game» (to "natural-number-game") # «.real-number-game» (to "real-number-game") # «.mathlib-calculus» (to "mathlib-calculus") # «.tactics-in-ND» (to "tactics-in-ND") # «.vernacular» (to "vernacular") https://leanprover.github.io/ https://leanprover.github.io/tutorial/ https://leanprover.github.io/download/debian78.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # Dependencies sudo apt-get install libstdc++-4.8-dev libgmp-dev libmpfr-dev liblua5.2-dev ninja-build sudo dpkg -i /tmp/lean*.deb # (find-status "lean") # (find-vldifile "lean.list") # (find-udfile "lean/") # (find-sitelispfile "lean/") # (find-sitelispfile "lean/lean-mode.el") # (find-sitelispfile "lean/lean-mode.el" ";; Automatically use lean-mode for") # (find-sitelispfile "lean/load-lean.el") # (find-fline "/usr/lib/lean/") # (find-fline "/usr/lib/lean/hott/") # (find-fline "/usr/lib/lean/hott/book.md") # (find-fline "/usr/lib/lean/library/") # (find-fline "/usr/lib/lean/library/logic/logic.md") https://leanprover.github.io/documentation/ http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf https://leanprover.github.io/tutorial/tutorial.pdf https://leanprover.github.io/tutorial/quickref.pdf https://github.com/leanprover/lean https://github.com/leanprover/lean/blob/master/doc/lean/tutorial.org https://github.com/leanprover/lean/blob/master/src/emacs/README.md https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ *** https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/ https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ https://xenaproject.wordpress.com/2020/04/30/the-invisible-map/ https://xenaproject.wordpress.com/2020/06/27/teaching-dependent-type-theory-to-4-year-olds-via-mathematics/amp/ https://xenaproject.wordpress.com/2021/01/21/formalising-mathematics-an-introduction/ pictures as eefective guides *** https://xenaproject.wordpress.com/2021/04/18/induction-on-equality/ ##### # # regular-install-2021 # 2021jul05 # ##### # «regular-install-2021» (to ".regular-install-2021") # https://leanprover-community.github.io/get_started.html#regular-install # https://leanprover-community.github.io/install/debian.html * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) # (find-fline "~/usrc/lean-regular-install/") rm -Rv ~/usrc/lean-regular-install/ mkdir ~/usrc/lean-regular-install/ cd ~/usrc/lean-regular-install/ wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh bash install_debian.sh |& tee obids rm -f install_debian.sh && source ~/.profile wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh # bash elan-init.sh -y # (find-fline "~/usrc/lean-regular-install/install_debian.sh") # (find-fline "~/usrc/lean-regular-install/elan-init.sh") # (find-fline "~/usrc/lean-regular-install/obids") # (find-fline "~/usrc/lean-regular-install/obids" "No module named pip") # (find-fline "~/.local/bin/" "leanproject") # (find-fline "~/.local/pipx/") # (find-fline "~/.local/pipx/venvs/mathlibtools/") # (find-fline "~/.local/pipx/venvs/mathlibtools/bin/leanproject") # (find-fline "~/.profile" "$HOME/.elan/bin") # (find-fline "~/.elan/") # (find-fline "~/.elan/bin/" "lean") ~/.elan/bin/lean ~/.elan/bin/lean -h * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) leanproject # Traceback (most recent call last): # File "/home/edrx/.local/bin/leanproject", line 5, in <module> # from mathlibtools.leanproject import safe_cli # ModuleNotFoundError: No module named 'mathlibtools' cd find .elan .local | grep -i lean | sort ##### # # lean-3.4.2 # 2022dec22 # ##### # «lean-3.4.2» (to ".lean-3.4.2") # https://github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) rm -Rv ~/usrc/lean-3.4.2-linux/ tar -C ~/usrc/ -xvzf \ $S/https/github.com/leanprover/lean/releases/download/v3.4.2/lean-3.4.2-linux.tar.gz cd ~/usrc/lean-3.4.2-linux/ # (code-c-d "leanl" "~/usrc/lean-3.4.2-linux/") # (find-leanlfile "") https://github.com/leanprover/lean/archive/refs/tags/v3.4.2.tar.gz ##### # # vscode # 2021jul05 # ##### # «vscode» (to ".vscode") # (find-status "code") # (find-vldifile "code.list") # (find-udfile "code/") # (find-fline "/usr/share/code/") # (find-fline "/usr/share/code/bin/code") • (eepitch-shell) • (eepitch-kill) • (eepitch-shell) aptrm code sudo apt-get autoremove ##### # # delete-lean # 2021aug01 # ##### # «delete-lean» (to ".delete-lean") * (eepitch-shell) * (eepitch-kill) * (eepitch-shell) aptrm code ##### # # lean-mode # 2021jul05 # ##### # «lean-mode» (to ".lean-mode") # (find-epackages 'lean-mode) # (find-epackage-links 'lean-mode) # (find-epackage 'lean-mode) # (code-c-d "leanmode" "~/.emacs.d/elpa/lean-mode-20210502.2049/") # (find-leanmodefile "") # (find-leanmodegrep "grep --color=auto -nH --null -e rootdir *.el") # (find-efunction 'lean-get-rootdir) https://leanprover.github.io/documentation/ http://leanprover.github.io/presentations/20150123_lean-mode/lean-mode.pdf https://leanprover.github.io/tutorial/tutorial.pdf https://leanprover.github.io/tutorial/quickref.pdf ##### # # topos # 2021jul05 # ##### # «topos» (to ".topos") # https://github.com/b-mehta/topos # (find-git-links "https://github.com/b-mehta/topos" "topos") # (code-c-d "topos" "~/usrc/topos/") # (find-toposfile "") # (find-toposfile "README.md") # (find-toposfile "src/") # (find-toposfile "src/applications/") # (find-toposfile "src/category/") ##### # # diagram-chasing # 2021jul05 # ##### # «diagram-chasing» (to ".diagram-chasing") # (find-books "__cats/__cats.el" "himmel") # (find-himmeldiagchpage 19 "3.2. A formal proof of the four lemma") # (find-himmeldiagchtext 19 "3.2. A formal proof of the four lemma") ##### # # Theorem Proving in Lean # 2021oct01 # ##### # «theorem_proving_in_lean» (to ".theorem_proving_in_lean") ;; <tpinlean> ;; https://leanprover.github.io/theorem_proving_in_lean/ ;; https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf ;; (find-fline "$S/https/leanprover.github.io/theorem_proving_in_lean/") (code-pdf-page "tpinlean" "$S/https/leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf") (code-pdf-text "tpinlean" "$S/https/leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf") ;; (find-tpinleanpage) ;; (find-tpinleantext) ;; (find-tpinleanpage (+ 6 1) "1 Introduction") ;; (find-tpinleanpage (+ 6 1) "1.1 Computers and Theorem Proving") ;; (find-tpinleanpage (+ 6 2) "1.2 About Lean") ;; (find-tpinleanpage (+ 6 2) "1.3 About this Book") ;; (find-tpinleanpage (+ 6 3) "1.4 Acknowledgments") ;; (find-tpinleanpage (+ 6 5) "2 Dependent Type Theory") ;; (find-tpinleanpage (+ 6 5) "2.1 Simple Type Theory") ;; (find-tpinleanpage (+ 6 7) "2.2 Types as Objects") ;; (find-tpinleanpage (+ 6 9) "2.3 Function Abstraction and Evaluation") ;; (find-tpinleanpage (+ 6 11) "2.4 Introducing Definitions") ;; (find-tpinleanpage (+ 6 13) "2.5 Local Definitions") ;; (find-tpinleanpage (+ 6 13) "2.6 Variables and Sections") ;; (find-tpinleanpage (+ 6 15) "2.7 Namespaces") ;; (find-tpinleanpage (+ 6 17) "2.8 Dependent Types") ;; (find-tpinleanpage (+ 6 19) "2.9 Implicit Arguments") ;; (find-tpinleanpage (+ 6 21) "2.10 Exercises") ;; (find-tpinleanpage (+ 6 23) "3 Propositions and Proofs") ;; (find-tpinleanpage (+ 6 23) "3.1 Propositions as Types") ;; (find-tpinleanpage (+ 6 25) "3.2 Working with Propositions as Types") ;; (find-tpinleanpage (+ 6 27) "3.3 Propositional Logic") ;; (find-tpinleanpage (+ 6 31) "3.4 Introducing Auxiliary Subgoals") ;; (find-tpinleanpage (+ 6 32) "3.5 Classical Logic") ;; (find-tpinleanpage (+ 6 33) "3.6 Examples of Propositional Validities") ;; (find-tpinleanpage (+ 6 35) "3.7 Exercises") ;; (find-tpinleanpage (+ 6 37) "4 Quantifiers and Equality") ;; (find-tpinleanpage (+ 6 37) "4.1 The Universal Quantifier") ;; (find-tpinleanpage (+ 6 39) "4.2 Equality") ;; (find-tpinleanpage (+ 6 42) "4.3 Calculational Proofs") ;; (find-tpinleanpage (+ 6 43) "4.4 The Existential Quantifier") ;; (find-tpinleanpage (+ 6 48) "4.5 More on the Proof Language") ;; (find-tpinleanpage (+ 6 49) "4.6 Exercises") ;; (find-tpinleanpage (+ 6 53) "5 Tactics") ;; (find-tpinleanpage (+ 6 53) "5.1 Entering Tactic Mode") ;; (find-tpinleanpage (+ 6 56) "5.2 Basic Tactics") ;; (find-tpinleanpage (+ 6 60) "5.3 More Tactics") ;; (find-tpinleanpage (+ 6 62) "5.4 Structuring Tactic Proofs") ;; (find-tpinleanpage (+ 6 68) "5.5 Tactic Combinators") ;; (find-tpinleanpage (+ 6 70) "5.6 Rewriting") ;; (find-tpinleanpage (+ 6 72) "5.7 Using the Simplifier") ;; (find-tpinleanpage (+ 6 77) "5.8 Exercises") ;; (find-tpinleanpage (+ 6 79) "6 Interacting with Lean") ;; (find-tpinleanpage (+ 6 79) "6.1 Importing Files") ;; (find-tpinleanpage (+ 6 80) "6.2 More on Sections") ;; (find-tpinleanpage (+ 6 82) "6.3 More on Namespaces") ;; (find-tpinleanpage (+ 6 84) "6.4 Attributes") ;; (find-tpinleanpage (+ 6 85) "6.5 More on Implicit Arguments") ;; (find-tpinleanpage (+ 6 87) "6.6 Notation") ;; (find-tpinleanpage (+ 6 89) "6.7 Coercions") ;; (find-tpinleanpage (+ 6 89) "6.8 Displaying Information") ;; (find-tpinleanpage (+ 6 91) "6.9 Setting Options") ;; (find-tpinleanpage (+ 6 91) "6.10 Elaboration Hints") ;; (find-tpinleanpage (+ 6 92) "6.11 Using the Library") ;; (find-tpinleanpage (+ 6 95) "7 Inductive Types") ;; (find-tpinleanpage (+ 6 96) "7.1 Enumerated Types") ;; (find-tpinleanpage (+ 6 98) "7.2 Constructors with Arguments") ;; (find-tpinleanpage (+ 6 101) "7.3 Inductively Defined Propositions") ;; (find-tpinleanpage (+ 6 102) "7.4 Defining the Natural Numbers") ;; (find-tpinleanpage (+ 6 105) "7.5 Other Recursive Data Types") ;; (find-tpinleanpage (+ 6 106) "7.6 Tactics for Inductive Types") ;; (find-tpinleanpage (+ 6 111) "7.7 Inductive Families") ;; (find-tpinleanpage (+ 6 113) "7.8 Axiomatic Details") ;; (find-tpinleanpage (+ 6 114) "7.9 Mutual and Nested Inductive Types") ;; (find-tpinleanpage (+ 6 115) "7.10 Exercises") ;; (find-tpinleanpage (+ 6 117) "8 Induction and Recursion") ;; (find-tpinleanpage (+ 6 117) "8.1 Pattern Matching") ;; (find-tpinleanpage (+ 6 120) "8.2 Wildcards and Overlapping Patterns") ;; (find-tpinleanpage (+ 6 122) "8.3 Structural Recursion and Induction") ;; (find-tpinleanpage (+ 6 124) "8.4 Well-Founded Recursion and Induction") ;; (find-tpinleanpage (+ 6 126) "8.5 Mutual Recursion") ;; (find-tpinleanpage (+ 6 128) "8.6 Dependent Pattern Matching") ;; (find-tpinleanpage (+ 6 130) "8.7 Inaccessible Terms") ;; (find-tpinleanpage (+ 6 131) "8.8 Match Expressions") ;; (find-tpinleanpage (+ 6 133) "8.9 Exercises") ;; (find-tpinleanpage (+ 6 135) "9 Structures and Records") ;; (find-tpinleanpage (+ 6 135) "9.1 Declaring Structures") ;; (find-tpinleanpage (+ 6 138) "9.2 Objects") ;; (find-tpinleanpage (+ 6 139) "9.3 Inheritance") ;; (find-tpinleanpage (+ 6 141) "10 Type Classes") ;; (find-tpinleanpage (+ 6 141) "10.1 Type Classes and Instances") ;; (find-tpinleanpage (+ 6 143) "10.2 Chaining Instances") ;; (find-tpinleanpage (+ 6 144) "10.3 Inferring Notation") ;; (find-tpinleanpage (+ 6 145) "10.4 Decidable Propositions") ;; (find-tpinleanpage (+ 6 147) "10.5 Managing Type Class Inference") ;; (find-tpinleanpage (+ 6 149) "10.6 Coercions using Type Classes") ;; (find-tpinleanpage (+ 6 153) "11 Axioms and Computation") ;; (find-tpinleanpage (+ 6 154) "11.1 Historical and Philosophical Context") ;; (find-tpinleanpage (+ 6 154) "11.2 Propositional Extensionality") ;; (find-tpinleanpage (+ 6 155) "11.3 Function Extensionality") ;; (find-tpinleanpage (+ 6 157) "11.4 Quotients") ;; (find-tpinleanpage (+ 6 161) "11.5 Choice") ;; (find-tpinleanpage (+ 6 163) "11.6 The Law of the Excluded Middle") ;; (find-tpinleanpage (+ 6 167) "Bibliography") ##### # # natural-number-game # 2021oct06 # ##### # «natural-number-game» (to ".natural-number-game") # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html # https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html#sourcecode # https://github.com/ImperialCollegeLondon/natural_number_game # https://github.com/mpedramfar/Lean-game-maker # (find-git-links "https://github.com/ImperialCollegeLondon/natural_number_game" "nng") # (find-git-links "https://github.com/mpedramfar/Lean-game-maker" "lgm") # (code-c-d "nng" "~/usrc/natural_number_game/") # (code-c-d "lgm" "~/usrc/Lean-game-maker/") # (find-nngfile "") # (find-nngfile "docs/technical.md") # (find-nngfile "docs/technical.md" "tactic monad") # (find-nngfile "src/tactic/") # (find-nngfile "src/tactic/modded.lean") # (find-nngfile "src/game/") # (find-nngfile "src/game/world2/") # (find-nngfile "src/game/world2/level1.lean") # (find-lgmfile "") https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.youtube.com/watch?v=9V1Xo1n_3Qw LftCM2020: Natural number game - Kevin Buzzard https://xenaproject.wordpress.com/2019/10/24/chalkdust-and-the-natural-number-game/ https://xenaproject.wordpress.com/2019/11/12/the-natural-number-game-an-update/ ##### # # real-number-game # 2021oct17 # ##### # «real-number-game» (to ".real-number-game") # https://github.com/ImperialCollegeLondon/real-number-game # (find-git-links "https://github.com/ImperialCollegeLondon/real-number-game" "rng") # (code-c-d "rng" "~/usrc/real-number-game/") # (find-rngfile "") ##### # # mathlib-calculus # 2022jul03 # ##### # «mathlib-calculus» (to ".mathlib-calculus") # https://github.com/leanprover-community/mathlib # https://leanprover-community.github.io/mathlib_docs/ # https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html ;; <leanmathlib> ;; "The Lean Mathematical Library" ;; https://arxiv.org/abs/1910.09336 ;; https://arxiv.org/pdf/1910.09336.pdf (code-pdf-page "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") (code-pdf-text "leanmathlib" "$S/https/arxiv.org/pdf/1910.09336.pdf") ;; (find-leanmathlibpage) ;; (find-leanmathlibtext) # (find-anggsh "find . -mtime 0 | sort") # (find-fline "~/.config/Code/") # (find-fline "~/.local/pipx/logs/") # (find-fline "~/.elan/") # (find-fline "~/.local/pipx/") # (find-fline "~/.mathlib/") # (find-fline "~/.mathlib/url") # (find-fline "~/.vscode/") ##### # # tactics-in-ND # 2021oct14 # ##### # «tactics-in-ND» (to ".tactics-in-ND") # https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Deduction/near/257611457 # https://leanprover-community.github.io/mathlib_docs/tactic/explode.html#tactic.explode ##### # # vernacular # 2021dec16 # ##### # «vernacular» (to ".vernacular") # https://mathoverflow.net/questions/376839/what-makes-dependent-type-theory-more-suitable-than-set-theory-for-proof-assista # https://www.youtube.com/watch?v=Dp-mQ3HxgDE#t=1h0m0s Proposition world. A Proposition is a true/false statement, like 2 + 2 = 4 or 2 + 2 = 5. Just like we can have concrete sets in Lean like mynat, and abstract sets called things like X, we can also have concrete propositions like 2 + 2 = 5 and abstract propositions called things like P. Mathematicians are very good at conflating a theorem with its proof. They might say "now use theorem 12 and we're done". What they really mean is "now use the proof of theorem 12..." (i.e. the fact that we proved it already). Particularly problematic is the fact that mathematicians use the word Proposition to mean "a relatively straightforward statement which is true" and computer scientists use it to mean "a statement of arbitrary complexity, which might be true or false". Computer scientists are far more careful about distinguishing between a proposition and a proof. For example: x + 0 = x is a proposition, and add_zero x is its proof. The convention we'll use is capital letters for propositions and small letters for proofs. https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/FAQ.html https://github.com/ImperialCollegeLondon/natural_number_game https://github.com/mpedramfar/Lean-game-maker https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments/ Picking a basis and then pretending you didn’t https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/zulip.md https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Calling.20lean.20from.20command.20line https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf (find-books "__comp/__comp.el" "colton") https://leanprover.github.io/reference/ https://leanprover.github.io/reference/using_lean.html#using-lean-with-emacs https://lawrencecpaulson.github.io/2023/01/18/Sqrt2_irrational.html https://news.ycombinator.com/item?id=34437735 Formalising a new proof that the square root of two is irrational (lawrencecpaulson.github.io) *** # Local Variables: # coding: utf-8-unix # End: