{"id":"arxiv/2607.12981","url":"https://arxiv.org/abs/2607.12981","tags":["quant-ph"],"score":0,"title":"An Agentic Formalization for Certified Quantum Neural Network Design","domain":"quant-ph","source":"arxiv","authors":["Mingrui Jing","Lei Zhang","Yusheng Zhao","Hongshun Yao","Xin Wang"],"reviews":0,"subject":"quant-ph","summary":"A central model in quantum machine learning is the quantum neural network (QNN), whose design requires balancing expressivity and trainability. Technically, expressivity is studied through circuit-function analysis, such as quantum signal processing, while trainability is analyzed using dynamical-Lie-algebra (DLA) methods. To support certified QNN design, we formalize these major components of QNN theory in a connected lean 4 development checked by a proof kernel, where every analytic input is either proved or exposed as a named hypothesis. On the expressivity side, we prove exact…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-07-14","reactions":{}}