Isabelle/HOL中关于反问题结果的相对形式化
Relative formalization in Isabelle/HOL of a result in inverse problems
AI总结：
本研究利用Isabelle/HOL对arXiv:2606.15977中的反问题结果开展自动形式化实验，基于熟知的外部结果完成证明，相关文件已在GitHub仓库公开。
AI中文摘要：
本研究报告了一项使用Isabelle/HOL对arXiv:2606.15977中关于分段多项式各向异性电导率的反问题结果进行自动形式化的实验。该结果的证明基于多个被视为熟知且普遍接受的外部结果，形式化文件已在GitHub仓库提供，文中还讨论了翻译问题。
英文摘要：
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.
