Some more context on sat and first order solvers in math: the first open math problem solved autonomously by a computer was in 1997, well before the advent of generative ai.