Machine learning methods and unknotting numbers
Big-data and machine-learning-assisted searches attack both sides of unknotting number: finding short routes and proving that no shorter route can exist.
Coming soon: the arXiv page and the customary very unserious theme song.
Video
A short introduction to the project and its computational viewpoint.
Data
- Title: Machine learning methods and unknotting numbers
- Authors: Anne Dranowski, Zhen Guo, Yura Kabkov and Daniel Tubbenhauer
- Status: Preprint, 2026. 26 pages. Comments welcome.
- Code and (possibly empty) erratum: GitHub
- arXiv: coming soon
- Video: YouTube
- Slides: Sydney 2026 talk
- Theme song: coming soon
- MSC 2020: Primary: 57K10; Secondary: 68T05, 91A44.
Abstract
Determining the unknotting number requires both finding short unknotting sequences and proving that no shorter ones exist. We use big data and machine-learning-assisted searches for both upper and lower bounds, obtaining new exact unknotting numbers and a small Bernhard-Jablan-type counterexample, and discuss how games could help discover further bounds.
What is the point?
The unknotting number has two computationally different sides. An upper bound needs a route: a replayable sequence of crossing changes and diagram moves. A lower bound needs an obstruction: a finite certificate proving that every shorter route is impossible. This paper puts reinforcement learning, a language-model-assisted search, exact deterministic calculations and ordinary mathematical proofs into one workflow.
Find an explicit route and replay it.
Produce a finite obstruction certificate.
Make the constructive and obstructive bounds meet.
Main outputs
exact values
New exact unknotting numbers obtained when the improved lower bound meets the known upper bound.
successful obstructions
Alternating and nonalternating knots for which the paper rules out the previous lower endpoint.
a small counterexample
It has unknotting number two, but no reduced alternating minimal diagram reveals the required first crossing change.
The lower-bound engine combines a zero-class correction-term certificate for alternating knots with a Montesinos correction-term test for suitable nonalternating knots. The upper-bound side uses reinforcement-learning routes and diagram inflation.
How the lower-bound agent works
The language model chooses a promising knot, checks which theorem template applies and requests the exact data needed for a certificate. Deterministic code performs the finite calculation, and the resulting matrices, correction terms and comparison data are checked independently. Once the certificate has been produced, the language model is no longer part of the proof.
Match a database row to an obstruction.
Run exact finite arithmetic and retain certificate data.
Apply the theorem and independently rerun the check.
Unknot!
The game turns the upper-bound search into a public puzzle: players manipulate knot diagrams and produce routes that can be reconstructed and verified. In the paper this is also a future-facing experiment in citizen mathematics - human visual intuition supplies unusual attempts, while software keeps score and checks the output.
The first eight research levels. The current demo already contains three of them.
A few extra words
The project is deliberately not a claim that an AI system has replaced mathematical proof. Learning systems are used where they are useful: exploring large search spaces, proposing routes and selecting promising obstruction tests. The final outputs are conventional mathematical objects - explicit witnesses for upper bounds and exact finite certificates for lower bounds.