
GamePad: как учат нейросети доказывать теоремы в Coq
Исследователи предложили среду GamePad — обвязку вокруг Coq, где нейросеть учится доказывать теоремы шаг за шагом. Разбираем, как устроен подход и почему автодоказательство до сих пор упирается в данные.










