BruKnot: Learning Verifiable Constructions in the Reidemeister Graph

Useful auxiliary constructions can turn stalled mathematical search into routine deduction. Inspired by AlphaGeometry, we study this principle in knot simplification, where hard unknot diagrams require a temporary increase in crossings before reduction can begin. BruKnot alternates bounded symbolic simplification with language-model proposals of crossing additions and rearrangements. We first adapt a pretrained model to planar-diagram (PD) codes and elementary moves, then train it on escape constructions obtained by symbolic search. The combined training/validation corpus contains 2.53 million diagram–construction pairs. At inference, the symbolic engine checks proposals, retains executable prefixes, and resumes reduction. On 300 prospectively selected diagrams screened to exclude exact overlap with the audited fine-tuning corpora, BruKnot achieves a 70.3% mean solve rate across three inference seeds of one checkpoint, compared with 5.0% for a legal-random proposer using a fixed empirical length distribution, the same symbolic search, and matched permitted proposal opportunities. Every counted solution passes model-free replay, run afresh with the same patched symbolic kernel. The results support learned, state-dependent construction choices as useful search guidance, even when complete model proposals are not reliably executable.