Brouwer's fixed-point theorem is a famous result in mathematics stating that any continuous function mapping a compact, convex shape (like a square or ball) back to itself must have at least one fixed point, meaning some point that the function maps to itself. Weak König's lemma is a principle from logic saying that any infinite binary tree (a branching structure where each node splits into two) must contain an infinite path. Both of these are well-known results, but the question of how they relate to each other in a rigorous logical sense had not been fully settled.
The paper works within a field called constructive reverse mathematics, which asks: given a mathematical theorem, exactly which logical principles are needed to prove it, and which theorems are actually equivalent to each other? The goal is to pin down the precise logical strength of mathematical statements. The authors show that Brouwer's fixed-point theorem and weak König's lemma are equivalent, meaning each one can be used to prove the other.
The harder and more novel direction is deriving weak König's lemma from Brouwer's fixed-point theorem. To do this, the authors build on a construction originally due to the mathematician Orevkov, who showed that without certain logical assumptions, one can write down a continuous function on a square that has no fixed point. The authors extend and refine this construction so that the fixed points of a cleverly designed function encode whether an infinite path exists in a given tree. This turns the geometric statement about fixed points into a statement about infinite paths, completing the equivalence.