Toward a Lean Formalization of Analog Computing with Microwaves
Abstract
Analog computing with microwave signals can perform linear transformations directly in the analog domain, as the signals propagate through a microwave network. A fundamental question is which transformations can be computed with a given set of microwave components. In our previous work, we answered this question for networks of hybrid couplers and phase shifters by deriving a necessary and sufficient condition on the transformations these networks can compute, and we showed that the discrete Fourier transform (DFT) satisfies it. In this paper, we take a first step toward the formalization of analog computing with microwaves in Lean, a programming language and proof assistant that is increasingly adopted in mathematics. We formalize the considered components, their series and parallel connections, and the class of networks they can implement. Then, we formally prove the necessary and sufficient condition characterizing these networks, as well as the implementability of the DFT of any size power of two. All proofs are checked by the Lean kernel, and the code is openly available at: https://github.com/matteonerini/formalizing-analog-computing.
Related
- Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
- Formalization of Landau damping in the Vlasov--Poisson equations in Lean
- A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
- A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
- Formalization of Sullivan's No Wandering Domains Theorem in Lean
BibTeX
@misc{nerini2026toward,
title = {{Toward a Lean Formalization of Analog Computing with Microwaves}},
author = {Matteo Nerini and Xuekang Liu and Bruno Clerckx},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.04774},
eprint = {2610.04774},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.04774},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Toward a Lean Formalization of Analog Computing with Microwaves
AU - Matteo Nerini
AU - Xuekang Liu
AU - Bruno Clerckx
PY - 2026
DA - 2026/10/03
PB - arXiv
DO - 10.48550/arxiv.2610.04774
UR - https://arxiv.org/abs/2610.04774
AB - Analog computing with microwave signals can perform linear transformations directly in the analog domain, as the signals propagate through a microwave network. A fundamental question is which transformations can be computed with a given set of microwave components. In our previous work, we answered this question for networks of hybrid couplers and phase shifters by deriving a necessary and sufficient condition on the transformations these networks can compute, and we showed that the discrete Fourier transform (DFT) satisfies it. In this paper, we take a first step toward the formalization of analog computing with microwaves in Lean, a programming language and proof assistant that is increasingly adopted in mathematics. We formalize the considered components, their series and parallel connections, and the class of networks they can implement. Then, we formally prove the necessary and sufficient condition characterizing these networks, as well as the implementability of the DFT of any size power of two. All proofs are checked by the Lean kernel, and the code is openly available at: https://github.com/matteonerini/formalizing-analog-computing.
ER -