# Questions tagged [lean4]

Lean 4 is the latest major version of the Lean theorem prover by Microsoft Research. Use this tag for questions specific to Lean 4; if it's about Lean in general, use the tag (lean).

174 questions
Filter by
Sorted by
Tagged with
1 vote
24 views

### Passing functions to casesOn which do not depend on a pattern match

In Chapter 8 of Theorem Proving with Lean4, there's the following example of a tail function for dependent lists: ...
• 113
87 views

### Stochastic calculus in Lean4?

Has anyone started looking into this? Measures and Probability theory look like a good place to start, but maybe there are other resources? https://leanprover-community.github.io/undergrad.html
• 131
1 vote
43 views

### How to enter in Lean 4 the unicode for "LEFT SQUARE BRACKET WITH TICK IN TOP CORNER"

I am using Lean 4 (4.3) and trying to enter some stylized brackets in Unicode: ⦍ . Per this question, I tried to hover the mouse in VS Code over its definition: ...
• 2,320
175 views

### Could proof assistants fill in single theorems automatically?

Would it be possible to only write declarations and conclusions and write a program that automatically fill in theorems used to derive those conclusions in LEAN 4? From my understanding, proof ...
• 194
274 views

### What is the unicode braces {| |} (⦃ ... ⦄) in lean 4?

I came across the use of a Unicode braces here ⦃ ... ⦄ In Lean the definition looks like this: def Set.Subset (U V : Set α) : Prop := ∀ ⦃x⦄, x ∈ U → x ∈ V I am not sure what it is exactly. I know ...
• 2,320
133 views

• 2,320
1 vote
23 views

### Use of by on first line of lean proof - when to / when not to? [duplicate]

The following lean4 proof generates no warnings or errors. ...
• 119
57 views

### Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?

I have a Lean 4 test project in C:\Temp\MyProject I open with Visual Studio. In that directory, I have a Main.lean file. And, in ...
61 views

### How to combine the PROP of a list of PROP in lean 4?

I have the following structures: structure MyElem where identifier : Nat acceptable : Prop structure MyList where elements : List ( MyElem ) I want to ...
1 vote
54 views

### Showing that elements match after reducing list (Lean 4)

I'm currently trying to show that the elements of a reduced list match the original list after applying List.take. It feels obvious but it doesn't seem to be ...
1 vote
74 views

### Lean4: Prove that ∑ ii : Fin nn, k (Fin.castLE _ ↑↑ii) = ∑ x : Fin nn, k (Fin.castLE _ ↑↑x) (sums over Fin n)

Im working with sums over Fin n for some n : Nat, and I am stuck with two sums, that should be equal (and look exactly equal in ...
• 13
1 vote
133 views

### How can I reason backwards and assume the conclusion holds in Lean 4?

I was wondering how can one reason backwards in Lean 4, starting from an existentially quantified conclusion. I know that I can reason about an existentially quantified variable in a hypothesis using <...
• 2,320
1 vote
40 views

### Obtaining Elements in Linked Lists in Lean4

I am currently working on a proof involving chains in partially ordered sets in Lean right now, and am facing some issues regarding obtaining an element from a chain of arbitrary length (e.g. given a ...
83 views

### Transitivity of Implication in Lean 4

I'm trying to prove example (C A S: Prop) (h1 : C → A) (h2 : A → S) : C → S. It's this level in the Lean Intro to Logic game. So far I have ...
96 views

### What does "rintro rfl" do in LEAN?

Here is a block of LEAN code: ...
• 194
210 views

### When is the lean 4 "by" required?

I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally ...
• 2,320
38 views

1 vote
85 views

### Lean 4 directive to always include a section variable

Here is something that I think used to work in Lean 3, although I no longer have a working installation of Lean 3 with which to check that the details of this minimal example are precisely correct. I ...
• 1,051
101 views

### Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifier: In classical logic, ~∀x P(x) is equivalent to ∃x ~P(x). Looking at the existential quantifier in Lean4, the object ∃ x:nat P(x) is essentially the tuple (x:nat, P(...
543 views

### How does one import Natural numbers in Lean 4 -- unknown identifier 'ℕ'?

I found the definition of Nat's but lean still complains that it doesn't exist. Why is it? ...
53 views

### Pattern Matching on List x Fin

So, here is the example I'm working on: ...
• 165
149 views

### Lean4: How to construct an HEq between dependent functions?

I have an extremely simple goal to prove: HEq (fun px rd => match px, rd with | Sum.inr _ppos, dir => dir) fun x => id The reason the match ...
1 vote
71 views

### Termination for Wrapped Fin in Lean4

The following example type checks in Lean 4, but I am confused why the termination_by declaration is required. ...
• 165
80 views

### How to find the data type of a Json value that in lean4, to perform type validation. (Functional programming in lean)

Basically I am taking in a json object in lean4 as input and I want to check whether a particular feild like 'age' should always be Nat not something else depending on the schema that the user has ...
• 21
228 views

### For formal proofs of graph structures and algorithms, which proof assistant should I learn?

My goal is to be able to make formal proofs for graph structures and algorithms, proving i.e. for every vertex in a directed-acyclic-graph there exists a path from a source vertex to that vertex, or i....