Как устроено доказательство на Lean для программистов
Anatomy of a Lean proof for software engineers
Автор разбирает формальное доказательство на Lean для задачи из учебника Sipser: показать, что язык B, где нижняя строка битов равна сумме двух верхних, является регулярным. Вместо прямого построения DFA для B строится автомат для обратного языка B^R, читающий столбцы от младшего бита к старшему и запоминающий только перенос. Статья объясняет, как устроены спецификация, реализация и индуктивное доказательство в Lean, и почему это похоже на верификацию программ.
Хитрость в том, чтобы вспомнить, как вы складываете числа вручную: вы работаете от младшей значащей цифры к старшей. Единственное, что вы переносите из одного столбца в следующий, — это перенос.