Formalizing inverse problems in the age of AI: possibilities, pitfalls, and an invitation
AutoIP is described, a Lean library in which classical linear regularization theory, together with the functional analysis it rests on, has been autoformalized by AI agents, and a reviewer compares the formal statements with their natural-language counterparts and never needs to read a proof.
Christian Clason, Tapio Helin, M. Nursultanov et al.
· 0 citations