Logical Intelligence announces Slava Krushkal’s discovery
of the first new
“good group” in 31 years
Logical Intelligence announces Slava Krushkal’s discovery
of the first new
“good group” in 31 years
Foreword by eve bodnia
We’re excited to announce this discovery, not simply because it contributes directly to our company’s product development roadmap utilizing our in-house reasoning systems, but because our team brought deep mathematical intuition together with frontier models and our Aleph architecture to push forward on a problem in four‑dimensional manifolds that had been stagnant for three decades. Everyone brought something different to the table, from geometric insight and exploration to formalization and verification.
Even more exciting than the discovery itself is what it says about where human-machine collaborative reasoning can go next. As our reasoning systems become more capable, we believe that future generations of scientists and researchers will be able to tackle much deeper problems. Over time, that same approach will unlock progress in areas like materials, semiconductors, energy, and advanced engineering, places where breakthroughs require searching huge spaces, working within hard constraints, and making sense of incredibly complex systems. Slava Krushkal is a pioneer in what the future of human research supercharged by AI reasoning will look like. We are incredibly proud of Slava and the rest of Field Medalist Michael Freedman’s Discovery Team here at Logical Intelligence.
Topology is the study of shapes up to deformation - “rubber sheet geometry” - except the rubber sheets can be of any dimension d. It is one of the fundamental branches of mathematics along with analysis, logic, algebra, dynamics, number theory, and geometry. Because topology’s objects of study are so flexible and qualitative, it has been wondered if AIs will not be as effective in collaborating with topologists as they have with number theorists or analysts.
The rubber sheets of topology are more formally called manifolds M^d of dimension d. The case of surfaces is d=2. Manifolds were initially studied in connection with differential equations in the 19th century, but since 1900 have been a well defined subject of their own. There is a low dimensional theory, d=1,2,3 (dominated by geometry) and a high dimensional theory d=5,6,7,... (dominated by algebra). Then there is a mysterious world, d=4, which seems to its practitioners larger than all the rest combined; it is dominated by infinite processes. Here the 4D world splits in half according to whether the infinite processes have smooth limits, describable by differential equations, or have wild, merely topological limits, which are akin to Brownian motion, but quantitatively more wild. Remarkably, the wild world, called the topological category (TOP), has been easier to understand; it better fits the algebraic patterns of high dimensions: going wild allows construction of both examples and the isomorphisms between them, making the final answers quite systematic.
Topology is the study of shapes up to deformation - “rubber sheet geometry” - except the rubber sheets can be of any dimension d. It is one of the fundamental branches of mathematics along with analysis, logic, algebra, dynamics, number theory, and geometry. Because topology’s objects of study are so flexible and qualitative, it has been wondered if AIs will not be as effective in collaborating with topologists as they have with number theorists or analysts.
The rubber sheets of topology are more formally called manifolds M^d of dimension d. The case of surfaces is d=2. Manifolds were initially studied in connection with differential equations in the 19th century, but since 1900 have been a well defined subject of their own. There is a low dimensional theory, d=1,2,3 (dominated by geometry) and a high dimensional theory d=5,6,7,... (dominated by algebra). Then there is a mysterious world, d=4, which seems to its practitioners larger than all the rest combined; it is dominated by infinite processes. Here the 4D world splits in half according to whether the infinite processes have smooth limits, describable by differential equations, or have wild, merely topological limits, which are akin to Brownian motion, but quantitatively more wild. Remarkably, the wild world, called the topological category (TOP), has been easier to understand; it better fits the algebraic patterns of high dimensions: going wild allows construction of both examples and the isomorphisms between them, making the final answers quite systematic.
Figure 1. If two caps (drawn purple), intersecting a given cap, have different group elements or different dyadic labels, the cap may be split into two at the expense of increasing the genus of the base surface. The dual subgropes for the two new caps are parallel copies of the original one.
In addition to the pivot in technique, four‑dimensional manifolds sit at the crossroads of geometry, topology, and physics. Four is, of course, the coarse dimension of spacetime. The physical equations of Donaldson and Seiberg‑Witten rest on an analytic passage to the continuum; they give rise, in dimension four, to unprecedentedly fine distinctions of smooth structure. In contrast Topological constructions pioneered by Andrew Casson and Robert Edwards lead to a systematic theory of TOP, but one which stretches the very concept of continuity to its limit. When the two theories are combined the results are spectacular: an uncountable family of exotic smooth structures on the Euclidian space, R^4.
In addition to the pivot in technique, four‑dimensional manifolds sit at the crossroads of geometry, topology, and physics. Four is, of course, the coarse dimension of spacetime. The physical equations of Donaldson and Seiberg‑Witten rest on an analytic passage to the continuum; they give rise, in dimension four, to unprecedentedly fine distinctions of smooth structure. In contrast Topological constructions pioneered by Andrew Casson and Robert Edwards lead to a systematic theory of TOP, but one which stretches the very concept of continuity to its limit. When the two theories are combined the results are spectacular: an uncountable family of exotic smooth structures on the Euclidian space, R^4.
Figure 2. A branch with a free cap can be contracted across that cap without creating double points. After all such contractions, starting from a branch (a genus 1 part of the base surface) the construction of [KQ00, Section 4.1] gives an intersection tree of height h. Vertices correspond to branches and edges record intersections of caps.
This simplicity of TOP first emerged in my early work of the 4D Poincare conjecture, and was gradually extended to manifolds with more complicated fundamental groups 1 2 3. The question of whether TOP 4‑manifolds can be analysed by high dimensional techniques (called surgery theory) depends on the fundamental group \pi. This is the group of loops (starting and ending at an arbitrary base point) up to deformation, and under composition. The Poincare conjecture is about the sphere, where all loops are deformable to a point, so \pi is the trivial group. This is the easiest case! Historically 4‑manifold topologists call fundamental groups “good” if surgery theory applies. Despite much effort, the class of “good groups” has not budged since 1995. Now, with the AI‑assisted work of Slava Krushkal of the University of Virginia we have a new family of (previously studied) groups, certain Sturmian groups, which are provably good. Sturmian groups arise in the study of symbolic dynamics. Various frontier models (ChatGPT and Claude) have contributed to this development as well as our in‑house verification architecture Aleph. In this specific development Aleph’s role has been to supply a relative Lean 4 certificate of deduction soundness, relative to a Lean translation of classical results from dynamics and group theory.
Aleph architecture is an evolving platform which seeks maximal automation “orchestration” between user goals and powerful AI models. It has access to the Frontier Models (FMs) as well as in house latent architectures. Slava initially let Aleph loose on a small family of problems related to the fundamental issues of TOP. It generated promising proof plans but failed to close the loop. Slava, using his own wet‑brain intelligence took the reins and interacted directly with the FMs, chiefly Claude and ChatGPT, to piece together a proof that certain previously studied groups from a class called Sturmian, were good. After the construction of the proof at an informal level, the language models iterated to produce a Lean4 version, and finally after further iteration Aleph produced a Lean certificate with 0 sorrys (relative to its input, which consisted not only of the Lean kernel but also our translations of several theorems from the group theory and dynamics literature.)
As the models Aleph can call improve in power and modes of thought, more aspects of theorem proving can be handed over to it. In particular, geometric reasoning in high dimensions, presently a weakness of LLMs, could become more efficient with the development of latent reasoners and steps of the kind Slava need to do “by hand” may also be automated.
This remarkable advance is on one of multiple fronts that Slava has been pursuing with Logical Intelligence backing. It is still (as of today) remotely possible that all groups are good. However an even more ambitious front of Slava’s project is to prove that non-abelian free groups are not good. AIs have been remarkably powerful in analysing the math-games Slava has devised. But so far the allowed moves of these games are only those that humans (like Slava) have seen: 4‑manifold topology is a notoriously visual subject. It is natural to wonder if language models which think in words more than pictures can play a decisive role in the more visual aspects of invention.
Inspired by the work of Yann LeCun, our research at Logical Intelligence approaches this question broadly. We explore the power of formal methods using latent reasoning models across many applications seeking more encompassing and more efficient modes of reason. But imbuing an AI with the mathematical analog of spatial reasoning is still in the future. We know from Slava’s work that non‑abelian free groups cannot be good unless there is some “new move” that humans have not seen. Building a model capable of seeing it (if it exists) would represent progress in a new dimension of thought. But for the present work, Slava relied on his own wet intelligence to translate the “moves” he ‘saw’ into the generators of a discrete dynamical system, morphing the original problem closer to algebra and making it more tractable for his AI collaborators.
The current advance may be just the beginning, I’d like to see where the subject stands in the distant future - in one year. We congratulate Slava on his advance.
This simplicity of TOP first emerged in my early work of the 4D Poincare conjecture, and was gradually extended to manifolds with more complicated fundamental groups 1 2 3. The question of whether TOP 4‑manifolds can be analysed by high dimensional techniques (called surgery theory) depends on the fundamental group \pi. This is the group of loops (starting and ending at an arbitrary base point) up to deformation, and under composition. The Poincare conjecture is about the sphere, where all loops are deformable to a point, so \pi is the trivial group. This is the easiest case! Historically 4‑manifold topologists call fundamental groups “good” if surgery theory applies. Despite much effort, the class of “good groups” has not budged since 1995. Now, with the AI‑assisted work of Slava Krushkal of the University of Virginia we have a new family of (previously studied) groups, certain Sturmian groups, which are provably good. Sturmian groups arise in the study of symbolic dynamics. Various frontier models (ChatGPT and Claude) have contributed to this development as well as our in‑house verification architecture Aleph. In this specific development Aleph’s role has been to supply a relative Lean 4 certificate of deduction soundness, relative to a Lean translation of classical results from dynamics and group theory.
Aleph architecture is an evolving platform which seeks maximal automation “orchestration” between user goals and powerful AI models. It has access to the Frontier Models (FMs) as well as in house latent architectures. Slava initially let Aleph loose on a small family of problems related to the fundamental issues of TOP. It generated promising proof plans but failed to close the loop. Slava, using his own wet‑brain intelligence took the reins and interacted directly with the FMs, chiefly Claude and ChatGPT, to piece together a proof that certain previously studied groups from a class called Sturmian, were good. After the construction of the proof at an informal level, the language models iterated to produce a Lean4 version, and finally after further iteration Aleph produced a Lean certificate with 0 sorrys (relative to its input, which consisted not only of the Lean kernel but also our translations of several theorems from the group theory and dynamics literature.)
As the models Aleph can call improve in power and modes of thought, more aspects of theorem proving can be handed over to it. In particular, geometric reasoning in high dimensions, presently a weakness of LLMs, could become more efficient with the development of latent reasoners and steps of the kind Slava need to do “by hand” may also be automated.
This remarkable advance is on one of multiple fronts that Slava has been pursuing with Logical Intelligence backing. It is still (as of today) remotely possible that all groups are good. However an even more ambitious front of Slava’s project is to prove that non-abelian free groups are not good. AIs have been remarkably powerful in analysing the math-games Slava has devised. But so far the allowed moves of these games are only those that humans (like Slava) have seen: 4‑manifold topology is a notoriously visual subject. It is natural to wonder if language models which think in words more than pictures can play a decisive role in the more visual aspects of invention.
Inspired by the work of Yann LeCun, our research at Logical Intelligence approaches this question broadly. We explore the power of formal methods using latent reasoning models across many applications seeking more encompassing and more efficient modes of reason. But imbuing an AI with the mathematical analog of spatial reasoning is still in the future. We know from Slava’s work that non‑abelian free groups cannot be good unless there is some “new move” that humans have not seen. Building a model capable of seeing it (if it exists) would represent progress in a new dimension of thought. But for the present work, Slava relied on his own wet intelligence to translate the “moves” he ‘saw’ into the generators of a discrete dynamical system, morphing the original problem closer to algebra and making it more tractable for his AI collaborators.
The current advance may be just the beginning, I’d like to see where the subject stands in the distant future - in one year. We congratulate Slava on his advance.
1
1
Michael Freedman, The disk theorem for four-dimensional manifolds, Proceedings of the International Congress of Mathematicians (Warsaw, 1983), 647‑663, PWN, Warsaw, 1984
Michael Freedman, The disk theorem for four-dimensional manifolds, Proceedings of the International Congress of Mathematicians (Warsaw, 1983), 647‑663, PWN, Warsaw, 1984
2
2
Michael Freedman and Peter Teichner, 4‑manifold topology. I. Subexponential groups, Invent. Math. 122 (1995), 509‑529.
Michael Freedman and Peter Teichner, 4‑manifold topology. I. Subexponential groups, Invent. Math. 122 (1995), 509‑529.
3
3
Slava Krushkal and Frank Quinn, Subexponential groups in 4‑manifold topology, Geom. Topol. 4 (2000), 407‑430.
Slava Krushkal and Frank Quinn, Subexponential groups in 4‑manifold topology, Geom. Topol. 4 (2000), 407‑430.
4
4
Slava Krushkal, 4‑manifold topology and collision rank of groups, preprint
Slava Krushkal, 4‑manifold topology and collision rank of groups, preprint
5
5
Lean formalization, https://github.com/VKRUSHKAL/Symmetric_collision_rank
Lean formalization, https://github.com/VKRUSHKAL/Symmetric_collision_rank