TY  - RPRT
TI  - From Dag-Like Proofs to Boolean Circuits in Lean
AU  - Lorenzo Saraiva
AU  - Edward Hermann Haeusler
PY  - 2026
DO  - 10.4204/eptcs.449.13
UR  - https://arxiv.org/abs/2607.20186
ID  - 2607.20186
ER  -