Я не про теорию, а про Аппеля и Хакена (то есть про настоящие доказательства настоящих
теорем с помощью компьютера - толку от них, впрочем, мало, понимания они особо не
прибавляют). Такого сейчас уже довольно много - это когда компьютер используют
для обхода обширной комбинаторной структуры и проверки свойств в каждой вершине.

Почему "минимальных моделей" планарных графов получается так много (в отличие от
случая g > 0), и почему нельзя доказать, что они покрывают всё, непереборным
образом, совершенно непонятно до сих пор вроде. Это как если бы для доказательства
однозначности разложения на множители в кольце целых пришлось бы разбирать
50 разных случаев (не имеющих никакой самостоятельной ценности причем).

Что касается стратегий, они не особо помогают. Есть proof assistance типа Coq
или вот там на видео LEAN даже гораздо лучше, но они не слишком хороши -
гэпы (пропущенные за недостатком занудства) в совершенно прозрачных на глаз
математика доказательствах оно заполняет довольно хреново.

Поэтому и думают про deep learning.