Tarski Research

We build mathematical data for training and evaluating frontier models.

Mathematics is changing quickly. In 2026, AI systems produced a formally verified proof of finite-time blowup for the Navier–Stokes equations, one of the seven Millennium Prize Problems. Frontier models can now settle hard, well-posed problems, and Lean can check their work. The open question is whether they can meaningfully build mathematical theory in an open-ended fashion.

If you’re interested in mathematical data for your models, email us at nathan@tarskiresearch.com. More here soon.