Cabled arrow polynomials of virtual knots

Stream: lean4

[Kyle Miller]

I thought I'd share a program I'd been working on in Lean 4 to calculate some polynomial invariants of objects called virtual knots (they're more-or-less knot diagrams on surfaces): https://github.com/kmill/arrow_poly

I'd previously written programs in Mathematica and JavaScript to compute these, but the Mathematica implementation was too slow and I wanted more confidence in the JavaScript calculations, so I decided to do a clean-room reimplementation in Lean 4 -- that way if the two programs came up with the same results, they might both be right (and they agreed!). Due to time constraints, the theorem proving capabilities are only being lightly used, mostly to make sure certain program invariants are recorded here and there. There is certainly not a proof that this computes a virtual knot invariant.

The repository is a bit weird since I was also using this to practice writing some proofs in Lean 4. Also, since I only wanted to target a single set of goalposts rather than two, it's not making use of Mathlib4.

[Kyle Miller]

The Lean 4 implementation is significantly faster than the JavaScript implementation, and it computes what I wanted it to compute in a reasonable amount of time (it's sort of like it's computing Jones polynomials of 2500 45-crossing knots in 2.8 days of computer time, and Jones polynomials are very exponential in the number of crossings; the JavaScript implementation could, in comparison, only do 2500 20-crossing knots in 9.5 days of computer time). The next step would be doing essentially 80-crossing knots, but these computations take about 10 hours each with the current implementation.

[Henrik Böving]

Regardless of the impressive work I want to add that "cabled arrow polynomials of virtual knots" is probably the most sci-fi name I have ever seen for something mathematical :grinning:

[Patrick Massot]

One day we'll definitely need to formally verify the whole knot atlas, together with everything that SnapPea says. At some point we'll get there.

[Siddhartha Gadgil]

To clarify, when you benchmark are these the times in the interpreter, or run after building a binary? The latter is enormously faster.

[Kyle Miller]

@Siddhartha Gadgil Yes, run after building a binary.

[Siddhartha Gadgil]

Thanks. This is very nice. Will look at it in detail.
To clarify again, was the JavaScript program for comparison on NodeJs (I mean mainly not run in the browser)?