💻 computer science

From Dag-Like Proofs to Boolean Circuits in Lean

This paper presents a method for encoding compressed Dag-Like Derivability Structures (DLDS) from Natural Deduction proofs in minimal logic as Boolean circuits, formally verifying their correctness and establishing a machine-checked bridge to circuit evaluation using the Lean theorem prover.

Original authors: Lorenzo Saraiva (Pontificia Universidade Catolica do Rio de Janeiro), Edward Hermann Haeusler (Pontificia Universidade Catolica do Rio de Janeiro)

Published 2026-07-23

📖 9 min read🧠 Deep dive

CC BY 4.0

Original authors: Lorenzo Saraiva (Pontificia Universidade Catolica do Rio de Janeiro), Edward Hermann Haeusler (Pontificia Universidade Catolica do Rio de Janeiro)

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to solve a massive, intricate puzzle where every piece is a logical argument. In the world of computer science and mathematics, this is called "formal verification." It's the process of proving that a computer program or a mathematical theorem is absolutely correct, with no hidden bugs or logical holes. To do this, mathematicians use "Natural Deduction," a step-by-step method of building proofs that looks a bit like a family tree. Every conclusion branches out from previous steps, creating a giant, sprawling tree of logic.

However, as these proofs get bigger, the trees get huge and messy. They contain a lot of repetition, like having the same branch grow out of the same spot over and over again. This makes checking the proof slow and difficult. To fix this, researchers use a technique called "horizontal compression." Imagine taking that giant tree and squishing it down so that identical branches merge into a single, shared path. The result isn't a tree anymore; it's a "Dag-Like Derivability Structure" (DLDS), which is basically a map where paths can cross and merge, saving a ton of space. But here's the tricky part: just because the map is smaller doesn't mean it's easy to read. Checking if a compressed map is still a valid proof is like trying to trace a single route through a tangled web of subway lines without getting lost.

This is where the story in the paper comes in. The authors, Lorenzo Saraiva and Edward Hermann Haeusler, ask a bold question: Can we turn this tangled, compressed map of a proof into something even simpler and more mechanical? They propose a way to translate these complex logical structures into "Boolean circuits." Think of a Boolean circuit not as a piece of silicon, but as a giant, rigid grid of light switches and wires. Instead of tracing a path through a messy graph, you just flip a set of switches (representing a potential path through the proof) and watch the lights. If the lights at the end turn on in the right pattern, the proof is valid. If not, it's invalid.

The paper presents a method to build this circuit for any compressed proof in a specific type of logic called "purely implicational minimal logic." They show that for any specific way of flipping the switches (a "path assignment"), the circuit correctly calculates whether that path follows the rules of logic. They didn't just guess this; they used a powerful computer tool called "Lean" to write a formal, machine-checked proof that their circuit construction works perfectly. It's like building a robot that can double-check the robot's own blueprints. While they haven't solved the problem of checking every possible path instantly (that would be too hard), they have proven that their circuit is a reliable, uniform way to check any single path you throw at it. This opens the door to using new, super-fast technologies, like quantum computers, to verify proofs in the future, turning the messy job of proof-checking into a clean, electrical game of on and off.

The Main Discovery: Turning Logic into a Light-Up Grid

The core achievement of this paper is the creation of a "uniform Boolean evaluation" for these compressed proofs. The authors took the complex rules that govern how a DLDS (the compressed proof map) works and translated them into a fixed grid of logic gates.

Imagine the proof as a city grid. In the old way, to check if a route is valid, you had to walk the streets, looking at every intersection and checking if the traffic lights were working correctly. This was slow and depended entirely on the specific layout of that one city. The authors' new method builds a giant, pre-fabricated grid where every possible street intersection exists as a potential "cell." You don't walk the city; instead, you hand the grid a set of instructions (a "path assignment") that says, "Turn on the lights for these specific streets and ignore the rest."

The circuit then acts like a massive, automated inspector. It checks two main things:

Is the route well-formed? Did you pick a valid sequence of logical steps (like Implication Introduction or Elimination)? If you picked a random street that doesn't connect to anything, the circuit flags it as "Invalid."
Are the assumptions discharged? In logic, you often start with a temporary assumption (like "Let's pretend X is true"). A valid proof must eventually prove that X doesn't matter anymore. The circuit tracks a "dependency bitstring"—a string of lights representing which assumptions are still active. If, at the very end of the route, all the lights are off (meaning no assumptions are left hanging), the circuit says "Accepted."

The paper proves that this circuit works perfectly for any single path you choose. They call this "pointwise correctness." It means that if you give the circuit a specific set of switch flips, it will tell you the truth about that specific path.

What the Paper Rules Out and Clarifies

It is crucial to understand what this paper does not claim, as the authors are very careful about this. They explicitly state that this method does not make checking the entire proof faster in the traditional sense.

The "global" condition—checking if the proof is valid for all possible paths—is still incredibly hard. The paper notes that the number of possible paths is exponential (it grows incredibly fast as the proof gets bigger). The circuit doesn't magically solve this massive calculation instantly. Instead, the authors reframe the problem: the circuit is a tool to check individual paths, and the "validity" of the whole proof is defined as the fact that every single one of those paths passes the check.

They also clarify that they are not claiming to improve on the existing "Flow" function (the standard way to check these proofs) for classical, step-by-step verification. The real value isn't in making the current check faster; it's in changing the format of the check. By turning the proof into a Boolean function (a giant on/off machine), they open the door for different kinds of verification methods, such as quantum computing techniques, which might be able to handle these massive "all paths" checks in ways traditional computers cannot.

How Sure Are They?

The authors are extremely confident, but in a very specific, rigorous way. They haven't just simulated this on a computer or guessed that it works. They have formally proved it.

Using the Lean proof assistant, they wrote a machine-checked verification of their entire construction. This means a computer has read their mathematical proof line-by-line and confirmed that there are no logical gaps.

Proven: The "pointwise correctness" is a mathematical fact. For any fixed path, the circuit behaves exactly as the logic requires.
Proven (with limits): They proved a "bridge" connecting this circuit back to the original proof structure, but only for a specific, simpler type of proof called the "uncompressed simple-tree fragment."
Future Work: They admit they have not yet proven the bridge for the fully compressed, complex cases involving "ancestor edges" and recursive flow conditions. They leave this as a task for future research.

The "Light-Up" Analogy in Action

To visualize this, imagine a giant, transparent board with thousands of tiny light bulbs arranged in a grid. Each row represents a step in the proof, and each column represents a different logical formula.

The Input: You have a remote control with a long list of buttons. Each button press tells the board which "wire" to light up between one row and the next. This is your "path assignment."
The Circuit: Inside the board, there are tiny logic gates. If you light up a wire that connects a "Premise A" to a "Premise B" to form a "Conclusion," the gate checks: "Does this match the rules of logic?" If you try to connect two things that don't fit, the gate stays dark or flashes a red error light.
The Output: At the very bottom of the board, there is a single "Goal" light. If you traced a path that followed all the rules and successfully "discharged" all your temporary assumptions, the Goal light turns green. If you missed a step or left an assumption hanging, the light stays red.

The paper's breakthrough is showing that you can build this board for any compressed proof, and the rules for how the lights behave are always the same, no matter how complex the proof is. It turns the abstract, messy art of logical deduction into a concrete, mechanical process of flipping switches and watching lights.

Why This Matters

While this might sound like a purely theoretical exercise, it has big implications for the future of computing. By translating proofs into Boolean circuits, the authors are speaking the native language of modern hardware. This makes it possible to use advanced technologies, like quantum computers, to verify proofs.

In the conclusion, the authors hint at a future where we might use "amplitude amplification" (a quantum technique) to search through the massive space of all possible paths to find the valid ones, or to prove that no invalid paths exist. They also mention that this could help in automated theorem proving, where computers try to find proofs for complex mathematical problems on their own.

The paper ends by acknowledging that while they have built the foundation (the circuit and the proof of its correctness for simple cases), the full house (the complex, compressed cases) is still under construction. But they have handed the builders a perfect blueprint, verified by a machine, showing exactly how to turn a tangled web of logic into a clean, electric grid.

Technical Summary: From Dag-Like Proofs to Boolean Circuits in Lean

Problem Statement
The paper addresses the challenge of efficiently verifying compressed proof representations, specifically Dag-Like Derivability Structures (DLDS), within purely implicational minimal logic ( $M^\supset$ ). DLDS are obtained by horizontally compressing Natural Deduction (ND) tree-like proofs, merging identical formulas at the same derivation level to reduce proof size while preserving logical correctness. While DLDS validity can be verified in polynomial time using a "Flow" function that propagates dependencies through the graph, this verification is tightly coupled to the specific topology of the DLDS. The authors identify a limitation: the Flow-based approach does not expose the verification condition as an explicit, uniform Boolean function that can be evaluated independently of the graph structure or reasoned about using alternative paradigms (such as quantum techniques). The goal is to reformulate the dependency-propagation check as a uniform Boolean evaluation problem.

Methodology
The authors propose a method to encode DLDS verification as a uniform Boolean evaluation problem over a fixed input domain. The core methodology involves three main steps:

Uniform Grid Construction: Instead of encoding a single derivation, the authors construct a Boolean circuit as a uniform grid based on the formula universe of the DLDS. If there are $N$ distinct formula labels, the circuit is an $N \times N$ grid where each row represents a derivation level and each column represents a formula. The grid contains "potential wires" connecting every cell at level $i$ to every cell at level $i+1$ . This grid acts as an over-approximation of the DLDS, containing all candidate local predecessor patterns.
Path Assignment and Subcircuits: The circuit input is a "path assignment," a tuple of $N$ $N$ independent traversals (subpaths), one for each formula column. These assignments dynamically select which potential wires are active. Each cell in the grid implements a local subcircuit that checks if the selected inputs correspond to a valid inference rule instance: Implication Introduction ( $\supset I$ $\supset I$ ), Implication Elimination ( $\supset E$ $\supset E$ ), or Repetition ( $R$ $R$ ).
- $\supset E$ : Computes the bitwise OR of incoming dependency sets.
- $\supset I$ : Computes the bitwise AND of the incoming set with the negation of the discharged assumption's bitstring.
- $R$ : Passes the dependency set unchanged (identity).
- Validity Check: Activation bits select the rule instance. An XOR gate enforces that exactly one rule is active; if the inputs do not determine a unique admissible rule, the path is marked as structurally invalid.
Acceptance Semantics: The circuit evaluates a pointwise acceptance bit, $acc_{D,c}(P)$ , for a given path assignment $P$ . The condition is satisfied if the path is either structurally invalid (assigned value 1 by definition to avoid false negatives in the universal check) or if it is well-formed and results in an empty dependency set at the goal column. The global acceptance condition is defined as the universal quantification over all possible path assignments: the DLDS is valid if and only if the circuit outputs 1 for every possible path assignment.

Key Contributions
The paper presents three primary contributions:

Reformulation of Verification: A shift from graph-traversal-based verification (Flow) to a uniform Boolean evaluation problem. This recasts the checking of candidate dependency-propagation paths as the evaluation of a fixed Boolean function over a domain of path assignments.
Polynomial-Size Circuit Construction: The construction of a Boolean circuit of size $O(N^3)$ (where $N$ is the number of subformulas) that computes the pointwise acceptance condition. The authors establish a pointwise correctness theorem, proving that for any fixed path assignment, the circuit's output matches the intended dependency-propagation semantics.
Lean Formalization: A machine-checked formalization in the Lean proof assistant. This includes:
- The circuit evaluator and its correctness theorems.
- Structural predicates for DLDS validity.
- A "bridge" theorem for the uncompressed simple-tree fragment. This theorem proves that a valid simple-tree DLDS (where no nodes are collapsed) satisfying route and discharge conditions yields genuine circuit acceptance of its extracted path.

Results

Pointwise Correctness: The authors prove that the constructed circuit correctly evaluates the validity of any single path assignment. If a path assignment corresponds to a valid derivation branch, the circuit outputs the correct dependency vector; if it corresponds to an invalid rule application, the circuit flags it.
Global Characterization: The global validity of a DLDS is characterized as the universal quantification of the pointwise condition over all path assignments. The authors clarify that this is a semantic specification rather than a polynomial-time classical decision procedure, as the space of path assignments is exponential.
Formal Verification: The Lean development successfully verifies the operational semantics of the circuit evaluator. The "bridge" theorem confirms that for the specific case of uncompressed simple-tree DLDS, the circuit-based evaluation aligns with the structural validity of the proof.

Significance and Claims
The paper claims significance in providing the first mechanized treatment of DLDS-to-circuit encoding in a proof assistant. By decoupling verification from the underlying graph structure, the approach offers a uniform Boolean encoding of proof validity. This is presented as a foundational step that makes the verification problem amenable to paradigms operating on Boolean functions rather than graph structures.

The authors explicitly state that this reformulation does not improve upon the classical Flow-based verification in terms of computational complexity for the global decision problem (which remains exponential in the path space). Instead, the value lies in the uniformity of the encoding. This uniformity potentially opens the door to alternative verification paradigms, such as quantum techniques (e.g., amplitude amplification) to decide whether the circuit computes the constant-1 function, a direction identified as future work. The current work focuses strictly on the classical construction and its machine-checked correctness, leaving the extension to the full compressed case (involving recursive Flow conditions, ancestor edges, and colors) for future research.