Alexander's theorem

Stream: Is there code for X?

[Michael Wahlberg]

Is there a code that proves Alexander's theorem from knot theory

[Yaël Dillies]

Hey! We are still pretty far from knot theory, but discussions are happening.

[Michael Wahlberg]

Also, do we canonically have a definition of grids in Lean4 / Lean3

[Yaël Dillies]

Pretty sure that no we don't

[Kevin Buzzard]

@Kyle Miller do you have a vision of knot theory in lean?

[Scott Morrison]

I think knot theory doesn't actually need particularly careful design ahead of time. There are many ways to represent knots, and we would eventually want all of them, and none need to be especially privileged. If someone wants to write the definition of the Alexander polynomial in terms of grid diagrams, or the Jones polynomial in terms of planar diagrams (PD notation), then either of those are wonderful even in isolation.

Later there will be theorems connecting them, and eventually connecting them to "actual" knots and Reidemeister moves.

[Scott Morrison]

I had a go a while back at defining the Jones polynomial, and ended up unhappy with several different attempts at it... There is the usual tension that one wants things dependently typed (e.g. by the size of the boundary of a tangle, or even the named endpoints around the boundary of tangle) but then nothing works smoothly. :-)

[Junyan Xu]

Prior discussion