dxdt.blog: занимательный интернет-журнал

В теоретической математике существует немало открытых проблем, которые пусть и не известны широкой публике, но всё же “широко известны среди специалистов”, то есть, достаточно знамениты, поскольку есть канонические списки (“Коуровская тетрадь” и др., не важно). Для заметной части из этих проблем и связанных задач можно было бы отыскать контрпримеры (и даже просто – примеры), используя современные возможности по оптимизированному перебору текстов компьютерных доказательств. В этом не только нет ничего особенно удивительного, но даже нет и проявления какого-то “нового интеллекта”: схема известная – перебирай себе тексты программ, проверяя автоматом корректность записи (см. историю проблемы о четырёх красках и так далее). Если бы, конечно, универсальным образом работал и перебор, и методы перевода на язык систем компьютерного доказательства нужных наборов теорем. Теоремы, впрочем, интенсивно переводят.

То есть, это самое реальное применение для знаменитых “LLM с нейросетками” на ближайшее время, при котором они могли бы оказаться очень эффективными для математических исследований. Попытки такие, вроде как, предпринимались, потому что подход достаточно очевидный, однако массового результата пока что не видно.

Адрес записки: https://dxdt.blog/2024/12/29/14572/