Lean

152 flashcards · Mathematics · by lakesare

1. The most promising of all theorem provers?

   Lean https://www.youtube.com/watch?v=Dp-mQ3HxgDE

2. What's formal verification?

   Mathematical proof that program woks.

3. Automated theorem proving VS interactive theorem proving?

   automated theorem proving - helps find a proof. Automated theorem proving focuses on the "finding" aspect. Resolution theorem provers, tableau theorem provers, fast satisfiability solvers, and so on provide means of establishing the validity of formulas in propositional and first-order logic. Other systems provide search procedures and decision procedures for specific languages and domains, such as linear or nonlinear expressions over the integers or the real numbers. Architectures like SMT (sa…

4. Is Lean automated theorem prover or interactive theorem prover?

   Lean tries to do both. There are two ways that a computer can help establish a claim: it can help find a proof in the first place (automated theorem proving), and it can help verify that a purported proof is correct (interactive theorem proving).

5. What logical system is Lean based on?

   A version of dependent type theory - Calculus of Constructions with inductive types. Dependent type theory is a powerful and expressive language, allowing us to express complex mathematical assertions, write complex hardware and software specifications, and reason about both of these in a natural and uniform way.

6. How to declare a natural number m in Lean?

   constant m : nat The #check command asks Lean to report their types; in Lean, commands that query the system for information typically begin with the hash symbol.

7. How to type this → nice arrow? Both notations work

   Just type \to.

8. What's this type?

   A type "function from ℕ to ℕ". If α and β are types, α → β denotes the type of functions from α to β.

9. What's this type?

   A type "Cartesian product ℕ × ℕ". If α and β are types, α × β denotes the cartesian product, that is, the type of ordered pairs consisting of an element of α paired with an element of β

10. Where could the parentheses be?

    When writing type expressions, arrows associate to the right; for example, the type of g is nat → (nat → nat). Thus we can view g as a function that takes natural numbers and returns another function that takes a natural number and returns a natural number. In type theory, this is generally more convenient than writing g as a function that takes a pair of natural numbers as input, and returns a natural number as output. For example, it allows us to "partially apply" the function g.

11. What would be the result of all these expressions?

    Type One way in which Lean’s dependent type theory extends simple type theory is that types themselves — entities like nat and bool — are first-class citizens, which is to say that they themselves are objects of study. For that to be the case, each of them also has to have a type.

12. What's the alternative notation for the Cartesian product?

13. How to write in Lean "function which maps any natural number x to x + 5"? For example, in mathematics it is common to say "let f be the function which maps any natural number x to x + 5".

14. What's the alternative way to write fun?

    λ

15. What comma (,) means here?

    λ x : nat { x + 5 } (Not real syntax, could also be written as λ (x : nat) { x + 5 })

16. Give an example of alpha-equivalent expressions. Formally, the expressions that are the same up to a renaming of bound variables are called alpha equivalent, and are considered "the same". Lean recognizes this equivalence.

    λ (x : ℕ), x λ (z : ℕ), z For example, the variable b in the expression λ (b : β) (x : α), x has nothing to do with the constant b declared earlier.In fact, the expression denotes the same function as λ (u : β) (z : α), z.

17. What does the #check command do?

    Same as typeOf. The #check command asks Lean to report their types; in Lean, commands that query the system for information typically begin with the hash symbol.

18. What's a nice way to think of types?

    Type == set (elements of the type are just the elements of the set).

19. [Kevin Buzzard talk] What would be a nice solution to formalize thousands of definitions in Lean?

    To feed the textbook to Lean, and use NLP.

20. What letters do we usually use to denote types?

    α, β, and γ

21. Where from does Lean infer the types of x and y in the last expression?

    From the functions h and f. Lean interprets the final three examples as the same expression; in the last expression, Lean infers the type of x and y from the types of f and h.

22. How to expand this syntax?

23. Alpha-equivalent VS beta-equivalent expressions?

    Alpha-equivalent expressions - just renaming of a bound variable. λ (x : ℕ), x ≡ λ (z : ℕ), z Formally, the expressions that are the same up to a renaming of bound variables are called alpha equivalent, and are considered "the same". For example, the variable b in the expression λ (b : β) (x : α), x denotes the same function as λ (u : β) (z : α), z.Beta-equivalent expressions - actual evaluation (λ v u x, v (u x)) g f a ≡ g (f a) The process of simplifying an expression (λ x, t) s to t[s/x] – t…

24. What does #reduce do?

    Performs beta reduction, and other reductions. The command #reduce tells Lean to evaluate an expression by reducing it to normal form, which is to say, carrying out all the computational reductions that are sanctioned by the underlying logic. But the #reduce command carries out other forms of reduction as well.

25. How should we read this?

    Place := 2 + 2 into y * y Replace every occurrence of y in y * y by 2 + 2.

26. Name 2 ways to define a function (with def).

    def double := (x) => { x + x } The general form of a definition is def foo : α := bar.def double(x) := x + x Lean also allows us to use an alternative format that puts the abstracted variables before the colon and omits the lambda.

27. What's the alternative syntax for: constant c: α def c: α := t As we have noted above, declaring constants in the Lean environment is a good way to postulate new objects to experiment with, but most of the time what we really want to do is define objects in Lean and prove things about them. The def command provides one important way of defining new objects.

    constant c: α - axiom def c: α := t - theorem, lemma

28. let a := t1 in t2 and (λ a, t2) t1 are similar, but how are these different? Notice that the meaning of the expression let a := t1 in t2 is very similar to the meaning of (λ a, t2) t1, but the two are not the same.

    let is much more powerful.

29. What would be the result?

    Type 1 Lean's underlying foundation has an infinite hierarchy of types.

30. What's "Type" an abbreviation for?

    Type 0

31. What's in common between list and prod functions?

    These functions accept types and return types.

32. What's a more concise way to write this?

    Use constant α : Type*. Equivalently, we can write Type _ or Type* to avoid giving the arbitrary universe a name. Throughout this book, we will generally use Type* in examples when we want type constructions to have as much generality as possible.

33. What n of arguments does this function have?

    6 arguments. α β γ are the first 3 arguments, function g, function f, x. => 8

34. What's a shorter way to write down these arguments? //=> 8

    Use variables.

35. Declaring a new constant is tantamount to?

    Declaring an axiomatic extension of our foundational system.

36. What does section do?

    Limits the scope of the variables. A variable stays in scope until the end of the file we are working on, and we cannot declare another variable with the same name. Sometimes, however, it is useful to limit the scope of a variable. For that purpose, Lean provides the notion of a section.

37. What's the difference between variables and constants?

    variables - simply insert the variables as bound variables when they are referred to, and discard of them when the file ends. constants - axiomatic extension! A variable stays in scope until the end of the file we are working on, and we cannot declare another variable with the same name.

38. What's the effect of namespace?

    You have to use foo.fa outside of the namespace.

39. What does "open" refer to?

    It opens up a namespace foo. When we declare that we are working in the namespace foo, every identifier we declare has a full name with prefix “foo.” Within the namespace, we can refer to identifiers by their shorter names, but once we end the namespace, we have to use the longer names.The open command brings the shorter names into the current context. Often, when we import a theory file, we will want to open one or more of the namespaces it contains, to have access to the short identifiers. Bu…

40. What's the difference between namespaces and sections?

    namespace - organize data section - declares temporary variables

41. What makes dependent type theory "dependent"?

    Because types depend on parameters. list ℕ and list bool are different!For another example, consider the type vec α n, the type of vectors of elements of α of length n. This type depends on two parameters: the type α : Type of the elements in the vector and the length n : ℕ.

42. Name 2 examples of Lean projects.

    mathlib While much Lean development takes place in the mathlib repository, there are many other projects using Lean that are developed and maintained by members of the community.Lean sudoku This is an implementation of sudoku, written in Lean. https://leanprover-community.github.io/lean_projects.html

43. What part of Lean is basically AI?

    Tactics. Also give reference on the ongoing research• AI is applicable to what kind of mathematics? An answer is behind in the discussion between Jason Rute and Johan Commelin in zulip chat. Tactics: https://leanprover.github.io/reference/tactics.htmlLean + OpenAI: https://openai.com/blog/formal-math/#fn2.

44. On what 2 parameters does the type vec depend on?

    α - type of elements in a vector b - number of elements in a vector

45. What does this theorem prove?

    Given: P P → Q Prove: Q The first line of the code states the theorem. Hypothesis h1 is that P is true, and hypothesis h2 is that P implies Q (note that Lean uses a regular arrow for implication rather than the more common ⇒ sign). The conclusion, after the colon, is that Q is true.The proof is between the begin and the end and it’s clear that it somehow uses both hypothesis h1 and hypothesis h2. But just reading the proof, it’s hard to see exactly what is going on. We can’t learn Lean this way.

46. Set theory VS type theory and Lean?

    Lean uses type theory as a foundation of mathematics rather than set theory.

47. [Type theory] Type VS term?

    type - collection of things (e.g. ℝ) term - element (e.g. 37) In Lean the type plays the role of the "collection of things", and the things in the type are called terms. For example, in Lean the real numbers ℝ are a type, not a set, and specific real numbers like 37 and 12345 are called terms of this type.

48. [Type theory VS set theory] How do we say 37 ∈ ℝ in type theory? In set theory, we write 37 ∈ ℝ to mean that 37 is a real number. More formally we might say "37 is an element of the set of real numbers".

    37 : ℝ In type theory the notation is different. In type theory we express the idea that 37 is a real number by writing 37 : ℝ, and more formally we would say "37 is a term of the type of real numbers". Basically the colon : in type theory plays the role of the “is an element of” symbol ∈ in set theory.

49. Name 3 levels of objects in Lean. The mental model which you should have in your mind is that in Lean, every object exists at one of three "levels".

    universes (e.g. Type) There are universes, such as Type, Prop.types (e.g. ℝ) There are types such as ℝ or G.terms (e.g. 37) There are terms such as 37 and g. Every mathematical object you know fits neatly into this hierarchy. For example rings, fields and topological spaces are all types in Lean, and their elements are terms.

50. Give an example of a proposition in Lean P : Prop.

    2 + 2 = 4 : Prop Lean regards a theorem statement as a type, not living in the Type universe, but in another universe called Prop – the universe of true-false statements.

51. h : 2 + 2 = 4 how should you read this what it really is?

    read this as - hypothesis is 2 + 2 = 4 reality - h is a term of the type 2 + 2 = 4 You could read it as the hypothesis that 2 + 2 = 4 or however you like, but under the hood what is happening is that h is a term of the type 2 + 2 = 4.

52. How to represent the type of the: nonnegative real number? When formalising mathematics one frequently runs into things like the type of non-negative real numbers.

    Give a pair (x, h) with: x: ℝ Real number xh: x ≥ 0 A proof h that x ≥ 0. To give a term of the type "nonnegative real number" is to give a pair (x, h) consisting of a real number x and a proof h that x ≥ 0, or, to put it in Lean's language, a term x : ℝ and a term h : x ≥ 0. When doing mathematics like this in Lean, one just gets used to the fact that some variables are representing elements of sets and others are representing proofs of propositions.

53. [Tactics] Name 3 tactics.

    apply exact intro If you’re just getting started, then try reading about intro, apply and exact. Those are the tactics you’ll need to solve the levels in the first problem sheet of the course, logic sheet 1 in section 1.

54. [Tactics] Conceptually - what does the intro tactic do?

    Makes the horizontal goal P → Q vertical. Changes P → Q goal to Q. The intro tactic makes progress on goals of the form ⊢ P → Q or ⊢ ∀ x, P x (where P x is any proposition that depends on x). Mathematically, it says “to prove that P implies Q, we can assume that P is true and then prove Q”, and also “to prove that P x is true for all x, we can let x be arbitrary and then prove P x.

55. [Tactics] Conceptually - what does the exact tactic do?

    Closes the goal. If your goal is ⊢ P then exact h will close the goal if h : P has type P. A common mistake amongst beginners is trying exact P to close a goal of type P. The goal is a type, but the exact tactic takes a term of that type, not the type itself. Remember : P is the statement of the problem. To solve the goal you need to supply the proof.

56. [Tactics] Conceptually - what does the apply tactic do?

    Moves the goal to something closer to the hypotheses. The apply tactic does one very specific thing, which I explain below. I have seen students trying to use this tactic to do all sorts of other things, based solely on the fact that they want to “apply a theorem” or “apply a technique”. The English word “apply” has far more uses than the Lean apply tactic. The apply tactic “argues backwards”, using an implication to reduce the goal to something closer to the hypotheses. apply h is like saying…

57. What do these mean: P: Prop VS h: P?

    P: Prop means that P is a property h: P means that h is a proof that P is true

58. What do these denote by convention?

    P, Q, R - propositions h, h1, hP - proofs or hypotheses

59. Name an instance of Curry-Howard isomorphism in Lean. Curry-Howard isomorphism is sometimes known as the propositions-as-types paradigm.

    p then q is the same as p → q. Moreover, once we make this identification, the rules for implication show that we can pass back and forth between implies p q and p → q. In other words, implication between propositions p and q corresponds to having a function that takes any element of p to an element of q. As a result, the introduction of the connective implies is entirely redundant: we can use the usual function space constructor p → q from dependent type theory as our notion of implication. Th…

60. Name 2 ways in which we can think of propositions as types.

    proposition p IS a data type; proof of p is an object of this data type proof : p. simple coding trick

61. How to: express a mathematical proposition p prove this proposition p

    express a mathematical proposition p - p : Prop In any case, all that really matters is the bottom line. To formally express a mathematical assertion in the language of dependent type theory, we need to exhibit a term p : Prop.prove this proposition p - t : p To prove that assertion, we need to exhibit a term t : p. Lean’s task, as a proof assistant, is to help us to construct such a term, t, and to verify that it is well-formed and has the correct type.

62. How to () P → Q → P? Note that `→` is not associative: in general `P → (Q → R)` and `(P → Q) → R` might not be equivalent.

    P → Q → P always means P → (Q → P). Just read from right to left!

63. [Tactics] Why is triv tactic called so?

    Because it's pretty trivial to prove true is true! Whenever the goal is true, we can prove it with triv. The triv tactic proves ⊢ true. It also proves goals of the form x = x and more generally of the form x = y when x and y are definitionally equal, but traditionally people use refl to do that.

64. [Tactics] What exactly does exfalso do?

    exfalso changes the goal of the main goal to false. The exfalso tactic changes your goal to false. Why might you want to do that? Usually because at this point you can deduce a contradiction from your hypotheses (for example because you are in the middle of a proof by contradiction).

65. [Tactics] Triv VS exfalso? True and false of lean tactics

    triv - whenever the goal is true, you can prove it with triv exfalso - changes the goal to false

66. [Tactics] What does change Q do?

    Changes the goal to Q if it's already definitionally equal to Q. If your goal is ⊢ P, and if P and Q are definitionally equal, then change Q will change your goal to Q.

67. [Tactics] Exfalso VS change Q?

    exfalso - changes the goal to false Whenever/change Q - changes the goal to Q Provided Q is definitionally equal to the current goal.

68. [Tactics] Conceptually - what does the by_contra tactic do?

    by_contra changes the goal to false (by introducing the opposite of the goal!)

69. [Tactics] Conceptually - what does the by_cases tactic do?

    Throws a truth table at our problem! All propositional logic problems can in theory be solved by just throwing a truth table at them. The by_cases tactic is a simple truth table tactic: by_cases P turns one goal into two goals, with P is assumed in the first, and ¬P in the second.

70. What's the definition of ¬ P in Lean? What is ¬ P definitionally equal to.

    ¬ P ≡ P → false

71. [Tactics] How to prove: numerical expression VS existential statement?

    numerical expression - norm_num existential statement - use

72. [Tactics] When to use ring VS norm_num?

    ring norm_num

73. [Tactics] How would you slay ∀ and ∃?

    slay ∀ - intro slay ∃ - use

74. [Tactics] refl vs rw?

    refl - closes A = A. refl stands for reflectivity.The refl tactic will close any goal of the form A = B where A and B are exactly the same thing.rw h - straightforward rewrite of the goal using h. rw stands for rewrite.Will look for the left hand side of h in the goal, and will replace it with the right hand side.

75. [Tactics] Name 2 ways to solve this with rw.

    rw h rw ← h

76. [Tactics] Split VS refine?

    split - splits P ∧ Q goal into 2 goals refine - a more refined split Faced with the goal ⊢ P ∧ Q, the split tactic will turn it into two goals ⊢ P and ⊢ Q.Faced with the goal ⊢ P ↔ Q, split will turn it into two goals ⊢ P → Q and ⊢ Q → P.Something which always amuses me – faced with ⊢ true, split will solve the goal. This is because true is made up of 0 subproofs, so split turns it into 0 goals.

77. [Tactics] How do we: split hypothesis VS split goal?

    split hypothesis - cases PQ with P Q split goal - split

78. [Tactics] What happens when we use ;?

    The part in { curly braces } keeps repeating until all goals get solved.

79. [Tactics] Name 2 tactics to prove P ∨ Q.

    left - ⊢ P right - ⊢ Q

80. [Tactics] How do we expand both h and goal?

    rw __________ at h ⊢

81. [Tactics] How to cheat in Lean?

    Just do library_search.

82. [Tactics] What kind of objects are: exact max_le_iff?

    exact - tactic max_le_iff - lemma

83. [Tactics] Name 2 ways to solve inequalities.

    linarith library_search

84. [Tactics] What tactic to apply to these hypotheses: ∀ ∃

    ∀ - specialize ∃ - cases

85. [Tactics] What tactic to apply to these goals: ∀ ∃

    ∀ - intro ∃ - use

86. [Tactics] How would we introduce a new hypothesis?

    have hypothesis_name : expression followed by the prove of the newly introduced hypothesis { ...proof... }

87. [Tactics] What does refl stand for?

    reflexivity

88. [Tactics] Visually imagine where to apply refl tactic.

    ⊢ a ~ b (where ~ is a reflexive operation)

89. [Tactics] What will rw h do?

    If h : x = y is a hypothesis then rw h changes all x in the goal to y.

90. In Lean, what's example VS theorem?

    example - theorem without name theorem - theorem with name Note that the theorem command is really a version of the def command: under the propositions and types correspondence, proving the theorem p → q → p is really the same as defining an element of the associated type. To the kernel type checker, there is no difference between the two.

91. Name 2 styles of proof in Lean.

    tactic-style proofs term-style proofs We will describe proofs that consist of sequences of tactics as "tactic-style" proofs, to contrast with the ways of writing proof terms we have seen so far, which we will call "term-style" proofs. Each style has its own advantages and disadvantages. For example, tactic-style proofs can be harder to read, because they require the reader to predict or guess the results of each instruction. But they can also be shorter and easier to write. Moreover, tactics of…

92. [Brackets in Lean] What do arguments in these brackets do: () {}/⦃⦄ [] mul_assoc : ∀ {G : Type} [self : mygroup G] (a b c : G), a * b * c = a * (b * c)

    () - what you need to pass yourself These are so called explicit arguments.{}/⦃⦄ - derived by Lean from (other arguments we passed). Figured out by Lean's unification system.We use {} when Lean can deduce { argument } to the function based on ( another argument we provided ). {} and ⦃⦄ differ in timing of the unifier.[] - derived by Lean from facts in mathlib. Figured out by Lean's type class inference system.We use [] when Lean can deduce [ argument ] based on facts from mathlib.

93. [Lean 3 vs Lean 4] Lean 3: fun x, x Lean 4: _______________?

    Lean 3: fun x , x Lean 4: fun x => x

94. [Lean] Visually imagine how propositions and their proofs relate to each other.

    proof: proposition "proof" has a type "proposition" To give a concrete example, we have 2 + 2 = 4 : Prop, because 2+2=4 is a true-false statement. we will learn in this course how to make a term h : 2 + 2 = 4; this term h should be thought of as a proof that 2+2=4. Every proposition in Lean has at most one term. The true propositions have one term, and the false propositions have no terms. We also have the proposition 2 + 2 = 5 : Prop. It is however impossible to make a term whose type is 2 + 2…

95. [Lean UI] Where is the "go to definition ↪" button defined?

    In mathlib (it's written in Lean).

96. [Lean UI] What does Lean use to implement VS Studio UI?

    Weird react. You can also open the developer view!! To produce the interface for this software, I also created the ProofWidgets system for Lean 3. This system is detailed in Chapter 5. The ProofWidgets system uses Lean's metaprogramming framework to allow users to write their own interactive, web-based user interfaces to display within the VSCode editor and in an online web-editor. The entire tactic state is available to the rendering engine, and hence expression structure and types of subexpre…

97. What is this a syntax sugar for?

    Simple functions can be defined using parentheses and · as a placeholder.

98. What is this a syntax sugar for?

99. What's the name of this operation |>? //=> 202 in all cases

    Forward pipeline. The forward pipeline |> operator takes a function and an argument and return a value. In contrast, the backward pipeline <| operator takes an argument and a function and returns a value.

100. What's: docstring VS docblock.

     docstring - fancy comments (can access via code) docblock - simple comments (but formatted)