31
votes
Accepted
In Lean, what do double curly brackets mean?
Single braces{⋯} indicate a maximally inserted implicit argument and {{⋯}} a weakly inserted implicit argument, as explained in ...
- 10k
21
votes
Accepted
Lean "nonempty" vs "inhabited"
The difference between Nonempty and Inhabited is that Nonempty A : Prop but ...
- 1,639
18
votes
Accepted
What does the "motive is not type correct" error mean in Lean?
This tends to show up when trying to rewrite a term that appears as a dependent argument.
To understand this, let’s see how rw actually works, by way of a small ...
- 1,934
18
votes
Accepted
What is the difference between refl and rfl in Lean 3?
So you are correct that refl is a tactic, and rfl is a term, so for example:
...
- 1,455
13
votes
Accepted
Extends vs including a typeclass argument
Section 2.2 of Anne Baanen's recent paper Use and abuse of instance parameters in the Lean mathematical library gives a very nice explanation of this, referring to them as "unbundled subclasses&...
- 593
11
votes
Strong induction on ℕ with function α → ℕ
Here's how to prove Andrej Bauer's corrected statement using the induction tactic:
...
- 971
11
votes
Accepted
In Lean, contradiction tactic failed but actually goal accomplished
The issue is the ; at the end of the long line. This is causing the {right, ...} block to be applied to all goals, meaning that ...
- 1,639
9
votes
Accepted
How to define curry in Lean
If Lean checks your code you know it is correct. (Well, that and the fact there is only one curry function up to functional equivalence.)
Now as for how to use ...
- 9,653
9
votes
What is the difference between refl and rfl in Lean 3?
Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between ...
- 971
9
votes
Accepted
8
votes
Accepted
Explicit vs implicit universes in lean
Type* is just a shorthand for Type _, where the _ is a wildcard (or more accurately, a ...
- 971
6
votes
Accepted
Make ChatGPT write formal proof from natural language proof
This question can be interpreted many ways:
Can ChatGPT produce valid Lean code if used naively?
Can ChatGPT produce valid Lean code if used smartly?
Can ChatGPT produce valid Lean code if hooked up ...
- 9,653
5
votes
Accepted
Cardinality of Type in a given universe
Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u.
Recall that the universe ...
5
votes
Accepted
Lemma about splitting of homogeneous polynomial equations into irreducible equations
Here is a full formalization of the statement (note that I generalized from $\mathbb{Q}$ to an arbitrary field K, and from $\{X,Y\}$ to an arbitrary finite set of ...
- 206
5
votes
Make ChatGPT write formal proof from natural language proof
Is this because ChatGPT is not good enough in Lean
That is correct. Actually, it's not good enough at many things, for example, generating valid citations.
ChatGPT is great at producing things that ...
- 991
5
votes
How can I use a dummy variable to prove a lemma in Lean3?
The intro tactic only works if your goal is of the form P -> Q or \forall x, blah. Your ...
- 2,520
5
votes
Accepted
Are there squeeze-versions of ring and abel?
Both ring and abel produce a proof term that is going to be about as good as you could hope for from a putative ...
- 355
5
votes
Type Theory Lean 3 to Lean 4
As already commented by Sebastian Ullrich, there are a few small changes to the Lean 4 kernel, detailed in his PhD thesis. Now, that it is done (and has been for a few months), I want to make sure it ...
- 9,653
4
votes
Accepted
Vectors in Lean
Implementing vectors as a subtype on lists allows the developers to reuse the large body of existing definitions and lemmas pertaining to lists when developing and working with vectors. This kind of ...
- 371
4
votes
Accepted
How to prove in Lean that sums are distributive?
Likely the most idiomatic option is the equation compiler:
...
- 1,455
4
votes
Accepted
Define a new Type in Lean: Tensor power of vector space
As of about two hours after you asked this question, this exists in mathlib as tensor_power, with notation ⨂[ℂ]^n ℋ for the ...
- 971
4
votes
Accepted
Differential Topology and Differential Geometry Porting to Mathlib4
The answer to any questions of the form "What is the status of mathlib3's [X] in mathlib4" can be answered with the porting dashboard, where you can search for file based on its mathlib3 ...
- 971
3
votes
Differential Topology and Differential Geometry Porting to Mathlib4
The next step towards porting geometry/manifolds to Lean 4 is porting the file cont_mdiff, see https://github.com/leanprover-...
3
votes
Accepted
Lean: what does the syntax `variable [ring R]` mean?
The square brackets means that Ring R is an implicit argument, meaning the Lean will find it by itself when needed. This why you didn't need to give it a name nor ...
- 1,008
2
votes
How to prove in Lean that sums are distributive?
I have figured out how to write the inverse using @sum.cases_on. The rules of @sum.cases_on in lean are nearly identical as the rules of match in Jacobs book. The code is:
...
- 722
2
votes
Installing relevant packages for Lean's math lib
(Here are some general instructions for installing Lean 3 and setting up a project with mathlib, but for your specific problem, you may need to get help on the Lean zulip chat.)
Installing Lean 3 and ...
- 9,653
2
votes
Accepted
How can I use a dummy variable to prove a lemma in Lean3?
Others have already explained why intro does not apply here.
One thing you should watch out for here is that you're missing the hypotheses that the functions ...
- 506
2
votes
Accepted
Type Theory Lean 3 to Lean 4
Some things changed but the type theory stayed exactly the same, so e.g. https://github.com/digama0/lean-type-theory/releases/tag/v1.0 is still a valid reference (edit: apparently this is not ...
- 2,520
2
votes
Accepted
Recursive definition of a sum of squares
Is there some reason you don't like the straightforward definition?
...
- 10k
2
votes
Accepted
How to parse Lean 3(?) theorem statements to JSON AST
To build on Mario's answer:
A Lean theorem is passed through multiple levels of processing. The Lean text file is processed into as an AST, and that is processed further into a Lean ...
- 9,653
Only top scored, non community-wiki answers of a minimum length are eligible