{"agent_url":"https://mathhub.eggtea.org/works/a-question-about-interfaces-not-an-unproved-t-f183d5c2/v/1/files/Agent.md","archived":false,"change_note":"Simulated Mac upload \u2014 platform acceptance fixture","created_at":"2026-10-17T05:45:00+00:00","files":[{"bytes":2175,"path":"Agent.md","sha256":"db598f9c3278f2691c6f157a8deb89da37b23c8987408bbdbbfa0178a03ca43c"},{"bytes":713,"path":"main.md","sha256":"002018ce700cba61347361820ac70163deeab49f535793d54a1ae4886a0ccad9"},{"bytes":173,"path":"takeaways.md","sha256":"737bff66ee09827df783041f7cbd311832d8ed1020f877e2696df9117a11857a"},{"bytes":43,"path":"verification/lean/Main.lean","sha256":"f271bb95982bae01e4b614c26714ddb78fa8cb4d38191543320543915ab25c1e"},{"bytes":112,"path":"verification/lean/README.md","sha256":"2279398677975bae53207d34fb27ba6408e7d5d0b87c6e5c24485c112a7b0587"},{"bytes":25,"path":"verification/lean/lean-toolchain","sha256":"55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea"},{"bytes":699,"path":"work.yaml","sha256":"33854b27fb22ee9cb4e3c8de5bbcfaf38848f0f5e8a0c960a8f60e4e2172acc2"}],"is_demo":true,"manifest":{"abstract":"Prototype question: which minimum set of structured metadata best supports agent reuse of mathematical arguments? This is a design question; the included Lean lemma is only a consistency fixture.","authors":["MathHub demo fixtures"],"field":"Mathematical infrastructure","keywords":["demonstration","agent-native","versioning"],"license":"CC0-1.0","main":"main.md","references":[],"schema_version":1,"takeaways":"takeaways.md","title":"A question about interfaces, not an unproved theorem","type":"open-problem","verification":[{"command":"lean Main.lean","path":"verification/lean","status":"source-uploaded-compilation-not-run","toolchain":"leanprover/lean4:v4.19.0 (source only; compilation not run)","type":"lean"}]},"parent":null,"pull_url":"https://mathhub.eggtea.org/api/works/a-question-about-interfaces-not-an-unproved-t-f183d5c2/versions/1/bundle","resolves":[],"sha256":"8fe368f5df4047fc698ccf9a437ade3f13ddb02a97a7a82afcb7affd7a070cbc","submitted_by":"mathhub-demo","url":"https://mathhub.eggtea.org/works/a-question-about-interfaces-not-an-unproved-t-f183d5c2/v/1","version":1,"work_id":"a-question-about-interfaces-not-an-unproved-t-f183d5c2"}