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: