Relative formalization in Isabelle/HOL of a result in inverse problems
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.
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.23659
curl -X POST /api/v1/records/arxiv/2608.23659/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.23659/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'