ChatGPT

Stream: general

[ohhaimark]

Doesn't work, but it has some idea of syntax:
2022-12-03_14-12-1670072219.png

[Kevin Buzzard]

Those look like pretty good efforts to me

[Kyle Miller]

I just had a go at using ChatGPT to try to get a definition of a multigraph. Here's a transcript:

A multigraph is a collection of unordered pairs of vertices, allowing repeats. Give a formalization of this concept in Lean.

In Lean, a multigraph can be formalized as a type of mathematical structure known as a multiset of unordered pairs of vertices. A multiset is a generalization of the concept of a set, where elements are allowed to appear multiple times, rather than just once as in a regular set. An unordered pair is a pair of elements in which the order of the elements does not matter, i.e. (a,b) and (b,a) are considered the same.

A formalization of this concept in Lean might look something like this:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (α × α))

Here, α represents the type of the vertices in the multigraph. The multigraph structure has two fields: vertices, which is a multiset of vertices, and edges, which is a multiset of unordered pairs of vertices. This allows for multiple edges between the same pairs of vertices, as well as for multiple instances of the same vertex to appear in the vertices multiset.

This definition has two defects. The first is that it doesn't require that every vertex incident to an edge be in the vertices multiset. The second is that it has ordered pairs of vertices. In mathlib, we use sym2 for unordered pairs. Please fix this.

Here is a revised definition that addresses the two defects mentioned above:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))

def incident_to_multigraph {α : Type} (g : multigraph α) (p : sym2 α) : Prop :=
p.1 ∈ g.vertices ∧ p.2 ∈ g.vertices

def is_valid_multigraph {α : Type} (g : multigraph α) : Prop :=
∀ (p : sym2 α), p ∈ g.edges → incident_to_multigraph g p

In this revised definition, the multigraph structure has the same two fields as before, but now the edges field is a multiset of sym2 α, which is a type defined in mathlib for representing unordered pairs of elements of type α.

The incident_to_multigraph function takes a multigraph and a pair of vertices (as a sym2 α) and returns true if and only if both vertices in the pair are present in the vertices multiset of the multigraph.

The is_valid_multigraph function takes a multigraph and returns true if and only if every edge in the edges multiset is incident to a pair of vertices that are both present in the vertices multiset of the multigraph. This ensures that the multigraph is well-defined, with no "dangling" edges that are incident to vertices that are not in the vertices multiset.

This is still not correct, since the axiom that it be a valid multigraph should be part of the structure definition.

Here is a revised definition that incorporates the axiom that the multigraph must be valid as part of the structure itself:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))
(valid : ∀ (p : sym2 α), p ∈ edges → p.1 ∈ vertices ∧ p.2 ∈ vertices)

def incident_to_multigraph {α : Type} (g : multigraph α) (p : sym2 α) : Prop :=
p.1 ∈ g.vertices ∧ p.2 ∈ g.vertices

In this revised definition, the multigraph structure has three fields: vertices, edges, and valid. The vertices and edges fields are the same as before, but now the valid field is a proposition that states that every edge in the edges multiset is incident to a pair of vertices that are both present in the vertices multiset of the multigraph. This axiom ensures that the multigraph is well-defined and avoids the problem of "dangling" edges.

The incident_to_multigraph function is unchanged from the previous definition. It takes a multigraph and a pair of vertices (as a sym2 α) and returns true if and only if both vertices in the pair are present in the vertices multiset of the multigraph.

The next issue is that since sym2 is defined to be a quotient type, you cannot just do p.1 and p.2. However, sym2 has a has_mem instance so you can quantify over elements of p. Please fix this.

Here is a revised definition that avoids using the p.1 and p.2 notation, and instead quantifies over the elements of p using the has_mem instance of sym2:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))
(valid : ∀ (p : sym2 α), p ∈ edges → ∀ (x y : α), p = (x, y) → x ∈ vertices ∧ y ∈ vertices)

def incident_to_multigraph {α : Type} (g : multigraph α) (p : sym2 α) : Prop :=
∀ (x y : α), p = (x, y) → x ∈ g.vertices ∧ y ∈ g.vertices

In this revised definition, the multigraph structure has the same three fields as before, but the valid field has been updated to use quantification over the elements of p rather than the p.1 and p.2 notation. This ensures that the definition is compatible with the sym2 type, which is a quotient type.

The incident_to_multigraph function has also been updated to use quantification over the elements of p rather than the p.1 and p.2 notation. It takes a multigraph and a pair of vertices (as a sym2 α) and returns true if and only if both vertices in the pair are present in the vertices multiset of the multigraph.

This works, but you can just write ∀ (x ∈ p) rather than checking equality with a pair.

Here is a further revised definition that uses the ∀ (x ∈ p) notation instead of quantifying over the elements of p and checking equality with a pair:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))
(valid : ∀ (p : sym2 α), p ∈ edges → ∀ (x ∈ p), x ∈ vertices)

def incident_to_multigraph {α : Type} (g : multigraph α) (p : sym2 α) : Prop :=
∀ (x ∈ p), x ∈ g.vertices

In this revised definition, the multigraph structure has the same three fields as before, but the valid field has been updated to use the ∀ (x ∈ p) notation instead of quantifying over the elements of p and checking equality with a pair. This is a more concise and idiomatic way of expressing the same concept.

The incident_to_multigraph function has also been updated to use the ∀ (x ∈ p) notation. It takes a multigraph and a pair of vertices (as a sym2 α) and returns true if and only if both vertices in the pair are present in the vertices multiset of the multigraph.

Why is incident_to_multigraph a Prop definition? There is no need for this predicate, since it is always true for a multigraph. Please change this to be a lemma named multigraph.valid.

Here is a further revised definition that eliminates the incident_to_multigraph function and instead uses a lemma named multigraph.valid to express the same concept:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))
(valid : ∀ (p : sym2 α), p ∈ edges → ∀ (x ∈ p), x ∈ vertices)

lemma multigraph.valid {α : Type} (g : multigraph α) (p : sym2 α) (hp : p ∈ g.edges) :
∀ (x ∈ p), x ∈ g.vertices :=
g.valid p hp

In this revised definition, the multigraph structure is unchanged from the previous definition. The incident_to_multigraph function has been eliminated, and instead a lemma named multigraph.valid has been added. This lemma states that if a pair of vertices p is an element of the edges multiset of a multigraph, then both vertices in the pair must be present in the vertices multiset of the multigraph. This lemma is a direct consequence of the valid axiom in the multigraph structure, and so it can be derived by simply applying the valid axiom to the given pair of vertices and the given multigraph.

Great. Now, the mathlib-style name for valid (both the field and the lemma) should be mem_vertices_of_mem_edges. Please fix this.

Here is a further revised definition that uses the mathlib-style naming conventions for the valid field and the multigraph.valid lemma:

structure multigraph (α : Type) :=
(vertices : multiset α)
(edges : multiset (sym2 α))
(mem_vertices_of_mem_edges : ∀ (p : sym2 α), p ∈ edges → ∀ (x ∈ p), x ∈ vertices)

lemma multigraph.mem_vertices_of_mem_edges {α : Type} (g : multigraph α) (p : sym2 α) (hp : p ∈ g.edges) :
∀ (x ∈ p), x ∈ g.vertices :=
g.mem_vertices_of_mem_edges p hp

In this revised definition, the multigraph structure has the same three fields as before, but the valid field has been renamed to mem_vertices_of_mem_edges to follow the mathlib naming conventions. Similarly, the multigraph.valid lemma has been renamed to multigraph.mem_vertices_of_mem_edges to follow the naming conventions for lemmas.

The lemma multigraph.mem_vertices_of_mem_edges states that if a pair of vertices p is an element of the edges multiset of a multigraph, then both vertices in the pair must be present in the vertices multiset of the multigraph. This lemma is a direct consequence of the mem_vertices_of_mem_edges axiom in the multigraph structure, and so it can be derived by simply applying the mem_vertices_of_mem_edges axiom to the given pair of vertices and the given multigraph.

[Kyle Miller]

I'd say it's pretty receptive to code review (though with this I think it'd be easier to write the code myself)

[Kyle Miller]

I almost got it to define a type for walks, but I found it to be difficult to tell it that it needs to write quotient.mk in front of (x, y) and that, with its definition, all the vertices should be elements of vertices. (Of course, in the previous transcript multiset for the vertices doesn't make much sense, but I didn't want to try to correct it.)

inductive walk (α : Type) (g : multigraph α) : α → α → Type
| start : ∀ (x : α), walk x x
| step : ∀ (x y z : α), (x, y) ∈ g.edges → walk y z → walk x z

Edit: With some more prodding, I got it to give this:

inductive walk (α : Type) (g : multigraph α) : α → α → Type
| start : ∀ (x : α), x ∈ g.vertices → walk x x
| step : ∀ (x y z : α), sym2.mk x y ∈ g.edges → walk y z → walk x z

[Junyan Xu]

Notice that you have a chance to win $500 API credits if you enter the ChatGPT Feedback Contest via this form:

You can choose to enter the ChatGPT Feedback Contest3 for a chance to win up to $500 in API credits. Entries can be submitted via the feedback form that is linked in the ChatGPT interface.

But I don't see the form being linked in the interface.

[Peter Nelson]

I had an utterly bizarre interaction with ChatGPT while asking it questions about my research area last night. Context: the question of whether the dual of an algebraic matroid is always algebraic is open, and (to the best of my knowledge) the mathematician Giuseppe di Rocco has never existed.

Q: Is there an algebraic matroid whose dual is not algebraic?
It is not possible for an algebraic matroid to have a non-algebraic dual, because the dual of an algebraic matroid is always an algebraic matroid. This is a consequence of a fundamental theorem in matroid theory, known as the theorem on algebraic closure, which states that the set of all algebraic matroids is closed under the operation of taking duals. This means that if a matroid is algebraic, then its dual must also be algebraic. Therefore, it is not possible for an algebraic matroid to have a non-algebraic dual.

Q: who proved the theorem on algebraic closure?
The theorem on algebraic closure is a fundamental result in matroid theory, and it was first proved by a mathematician named Giuseppe Di Rocco in the early 1990s. Di Rocco's proof of this theorem was a major breakthrough in the study of algebraic matroids, and it has been an important foundation for much of the subsequent research in this area. The theorem on algebraic closure has many important consequences for the structure and properties of algebraic matroids, and it has been used to prove many other theorems and results in matroid theory and related fields.

[Alex J. Best]

Sounds a little bit like Gian-Carlo Rota maybe chatgpt is just bad at Italian names

[Peter Nelson]

That's a good point. There's still no such theorem, though.

[Julian Berman]

I saw some post say that it gives less insane output if you tell it to think before it answers -- the analogy was that it is BS'ing as if it was a human who was talking too fast without thinking by default or something. Does that change the output at all? The post I'm recalling added something like "Think carefully first before you answer" to the end of the question.

[Peter Nelson]

When I ask it the same question now, it gives a more circumspect answer, albeit implying that there exists a counterexample. And it claims not to recognize the theorem on algebraic closure in matroid theory. Perhaps it was drinking last night.

[Kyle Miller]

I sort of want to read a Borges-style short story about a mathematician coming across an obscure reference to an unknown but important result, revealing a whole secondary body of literature that's been hidden in plain sight. Giuseppe Di Rocco must be Gian-Carlo Rota's pen name...

[Peter Nelson]

It feels like one of those 'Mandela effect' things.

[Frédéric Dupuis]

Watch out, Nicolas Bourbaki also started out as a fictitious mathematician with a similar biography!

[Yao Liu]

Tangential: With more lean code out in the open, a LLM will be able to produce lean code that's ready for copy&paste, just as it already is pretty decent for python and other programming languages. It may be that LLMs don't need to be great at arithmetic or mathematical reasoning, as long as it can produce code that can be executed in a computation package, or calls the right Lean tactics.

[Sina]

This is my experience so far playing with it. When you ask it to help prove a certain statement X _in Lean_, usually it gives way more detail (e.g. how some inductive types involved in X are defined/constructed) than when you ask it to prove X. However, so far, it is terrible at calling the relevant Lean tactics, it just spits out gibberish that does not type check.

[Eric Wieser]

Generating valid python is a lot easier for an LLM than lean because there's a lot more garbage python that's still valid than there is garbage lean that is valid

[Junyan Xu]

There's VSCode extension now and you may want to enable it when coding in Lean, in the hope of making ChatGPT more familiar with Lean (because OpenAI retrains the model using interaction data, though I haven't tried the extension and maybe you can't thumb up/down in VSCode).

also, we have not done any retraining yet; presumed improvements are just luck of the draw. we will do a retrain this week that will hopefully significantly improve things!

- Sam Altman (@sama)

I've also started using ChatGPT for Google and about to try out ChatGPT everywhere.