Измеренный ноль ценнее ненайденного правила

За один день три работы закончились «ничего не добавлено» — и каждая была полезнее половины успешных.

Поиск доказательств нашёл ноль из двадцати недоказанных утверждений. Не потому что плох (на контрольной задаче 11 из 11), а потому что искать нечем. Вывод: the-bottleneck-is-rule-strength.

Чтение условий если закрывает ноль целей — reading-if-conditions-closed-zero-goals.

Заказ на правило про модуль числа отвергнут, потому что заказанное утверждение ложно — nan-is-reachable.

Почему это ценно. Такой результат экономит работу, которую делали бы не туда. Он же переводит часть «долга перед прувером» в «нашу ошибку в постановке»: две функции уехали из списка «ядро не берёт» в список «утверждение ложно, и вот вход».

Самый сильный пример — 0 из 20 в замере цены доказательства (proof-cost-0-of-20). Ноль, полученный на воспроизводимой выборке и разложенный по причинам, дал план работ на неделю вперёд (no-induction-for-builtin-types) — чего не дало бы ни одно доказательство, добытое подбором удобной функции.

Требование к формулировке задач. Агенту надо прямо говорить: честное «не вышло, потому что вот это» — результат не хуже доказательства, и подгонять нельзя. Иначе он подгонит.

Связано: a-removal-must-turn-a-test-red, the-bottleneck-is-rule-strength