Skip to main content
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 ...
Andrej Bauer's user avatar
  • 9,523
21 votes
Accepted

Lean "nonempty" vs "inhabited"

The difference between Nonempty and Inhabited is that Nonempty A : Prop but ...
Mario Carneiro's user avatar
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: ...
It'sNotALie.'s user avatar
  • 1,445
16 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 ...
Joachim Breitner's user avatar
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&...
Rob Lewis's user avatar
  • 593
11 votes

Strong induction on ℕ with function α → ℕ

Here's how to prove Andrej Bauer's corrected statement using the induction tactic: ...
Eric's user avatar
  • 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 ...
Mario Carneiro's user avatar
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 ...
Jason Rute's user avatar
  • 8,825
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 ...
Eric's user avatar
  • 971
9 votes
Accepted

Strong induction on ℕ with function α → ℕ

...
Andrej Bauer's user avatar
  • 9,523
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 ...
Eric's user avatar
  • 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 ...
Jason Rute's user avatar
  • 8,825
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 ...
François G. Dorais's user avatar
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 ...
Junyan Xu's user avatar
  • 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 ...
Joey Eremondi's user avatar
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 ...
Kevin Buzzard's user avatar
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 ...
Kim Liesinger's user avatar
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 ...
Jason Rute's user avatar
  • 8,825
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 ...
Chris Bailey's user avatar
4 votes
Accepted

How to prove in Lean that sums are distributive?

Likely the most idiomatic option is the equation compiler: ...
It'sNotALie.'s user avatar
  • 1,445
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 ...
Eric's user avatar
  • 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 ...
Eric's user avatar
  • 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-...
Yury Kudryashov's user avatar
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 ...
Ricky's user avatar
  • 978
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: ...
Nico's user avatar
  • 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 ...
Jason Rute's user avatar
  • 8,825
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 ...
Kyle Miller's user avatar
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 ...
Kevin Buzzard's user avatar
2 votes
Accepted

Recursive definition of a sum of squares

Is there some reason you don't like the straightforward definition? ...
Andrej Bauer's user avatar
  • 9,523
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 ...
Jason Rute's user avatar
  • 8,825

Only top scored, non community-wiki answers of a minimum length are eligible