{"id":"arxiv/2608.23659","url":"https://arxiv.org/abs/2608.23659","tags":["math.AP"],"score":0,"title":"Relative formalization in Isabelle/HOL of a result in inverse problems","domain":"math.AP","source":"arxiv","authors":["Cătălin I. Cârstea"],"reviews":0,"subject":"math.AP","summary":"This reports on an experiment in autoformalization of arxiv:2606.15977, an inverse problems result for piecewise polynomial anisotropic conductivities, using Isabelle/HOL. The proof of the result is relative to a number of external results which were deemed to be well known and generally accepted to be true. The formalization files are made available at a GitHub repository. Translation issues are discussed.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-24","reactions":{}}