Экспериментальный инструмент для языка доказательств Lean 4, который автоматически строит только нужные теоремы о независимости операций.
Проект решает узкую техническую задачу для тех, кто пишет формальные доказательства в Lean 4: вместо того чтобы заранее доказывать все возможные пары теорем о том, что операции над данными не мешают друг другу (что становится непосильным при сотнях операций), система строит только те доказательства, которые реально понадобились, и запоминает их. Это прототип подхода к работе с крупными структурами данных в формальной верификации.
Описание автора:On-demand commutation theorems for state operations in Lean 4: a simproc plus realizable constants, so only the pairs proofs use are ever proved
