From Dag-Like Proofs to Boolean Circuits in Lean
Lorenzo Saraiva, Edward Hermann Haeusler
cs.LO
Jul 22, 2026 · v1
TL;DR
Formalizes in Lean a Boolean circuit evaluator for Dag-Like Derivability Structures, proving pointwise correctness and a simple-tree fragment bridge.
Abstract
In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.
Problem
Natural Deduction proofs in purely implicational minimal logic can be horizontally compressed into Dag-Like Derivability Structures (DLDS), directed acyclic graphs reducing redundancy. Establishing that such compressed structures correspond to Boolean circuits with verified correctness is nontrivial.
Approach
The authors define a construction encoding DLDS as Boolean circuits and establish pointwise correctness, showing the circuit agrees with the intended dependency-propagation semantics for any fixed path assignment. A Lean formalization provides machine-checked guarantees for the circuit evaluator. A restricted bridge for the uncompressed simple-tree fragment connects valid DLDS instances to circuit acceptance of extracted paths under route and discharge conditions.
Results
The Lean formalization establishes machine-checked correctness of the circuit evaluator and a verified bridge for the simple-tree fragment linking DLDS validity to circuit acceptance of extracted paths.
