Seminar Details

A central challenge in mathematical reasoning is finding the right auxiliary construction: a step that may not simplify a problem immediately, but makes further progress possible. Google DeepMind’s AlphaGeometry addresses this challenge in Euclidean geometry by combining symbolic reasoning with a learned model that proposes useful auxiliary constructions. Inspired by the same underlying principle, we will discuss BruKnot, a neuro-symbolic system for simplifying hard unknot diagrams. BruKnot combines symbolic search over Reidemeister moves with a fine-tuned language model that proposes short crossing-increasing and rearrangement sequences when ordinary simplification stalls.

We will discuss the overall architecture, the training-data pipeline, the interaction between learned guidance and symbolic search, current difficulties, and possible extensions to other mathematical domains for further development.