Hey, I'm Slava 👋
[email protected] · Google Scholar · Twitter · LinkedIn · GitHub
I was born in Vodorezovo, a Siberian village with a population of twenty. Since Vodorezovo was not heavily investing in AI research, I had to take a few detours before ending up in San Francisco, California.
Professionally, most people probably know me as a mathematician or a startup founder. It's fair although I do think it often overshadows my old career as a competitive Irish dancer.
As a mathematician, I worked on integrable lattice models, a fascinating subject in the intersection of mathematical physics, algebraic combinatorics, and representation theory. As a founder, I cofounded a startup in AI-driven drug discovery where we developed computational methods to predict results of expensive experiments using AI and physics-based methods.
As it happens, both of these plots are slightly out of date now.
These days I spend most of my waking hours wrangling AI models into solving hard math problems. Along the way, I'm formalizing chunks of algebraic combinatorics in Lean 4, contributing to the beautiful Mathlib, and researching how AI systems reason about and discover mathematics.
Recently I've been using these methods to find and formalize new mathematical results. A few of them:
- Erdős Problem 387. An unconditional covering construction that resolves a fifty-year-old question of Erdős and Graham on divisors of binomial coefficients, removing the dependence on GRH. Joint work with Hung Bui, Kyle Pratt, and Alexandru Zaharescu (arXiv), formalized in Lean 4.
- Influence–sensitivity tradeoff. A new best construction for the monotone influence–sensitivity tradeoff, improving the bound of O'Donnell–Servedio (2007), formalized in Lean 4.
- Prime-free prefixes of normal numbers. A base-ten normal number all of whose decimal prefix integers are composite, showing that normality alone cannot force prime prefixes. Paper and Lean 4 formalization.
Some writing: