Toward a Lean Formalization of Analog Computing with Microwaves
Matteo Nerini, Xuekang Liu, Bruno Clerckx
eess.SP
Oct 3, 2026 · v1
cs.IT physics.app-ph
TL;DR
Formalizes microwave networks of hybrid couplers and phase shifters in Lean 4 with Mathlib, proving their computability characterization and DFT implementability.
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.
Problem
Microwave linear analog computers (MiLACs) built from hybrid couplers and phase shifters compute linear transformations. Earlier work characterized which transformations such networks can compute, but results that hold over all network sizes and topologies cannot be checked by simulation or measurement.
Approach
Networks are modeled in Lean as n×n complex matrices, using their transmission scattering matrices. Interconnections, phase shifters, permutation networks and hybrid couplers are defined, along with series and parallel composition and an inductive class of implementable networks. A layered decomposition into permutation matrices and block-diagonal phase blocks is formalized using Mathlib matrix constructions. DFT implementability is proved by induction on the size exponent, following the radix-2 FFT butterfly structure.
Results
The Lean kernel checks proofs of the necessary and sufficient condition characterizing implementable networks, and of implementability of the DFT for every power-of-two size. Claude assisted in developing the code, which is openly available.
