{"schema_version":1,"research_id":"eoa_inverse_innovation_exp06_external_evaluation_20260803","source_assessment_id":"representation_independent_interface_contract__mathematics:P3:v0","cell_id":"representation_independent_interface_contract__mathematics","search_queries":["site:arxiv.org nonlinear inequalities formal verification certificate branch and bound exact rational Hales Solovyev","standard proof certificate format solver independent proof checker Alethe SMT proof","computer assisted proof inequality interval arithmetic certificate exact rational checker","mathematics journal policy computer assisted proofs reproducibility code data","proof certificate nonlinear inequality branch and bound box subdivision exact rational certificate checker","formal certificate global optimization interval branch and bound proof checker certificate format","site:hal.science certificate nonlinear inequalities interval arithmetic Coq exact rational proof","Flyspeck nonlinear inequality certificate branch tree proof format","\"A Safe Computational Framework for Integer Programming\" rational branch-and-bound certificate independent checker ACM","site:dl.acm.org 10.1145/3485630 branch-and-bound certificate checker","Flyspeck project completed formal proof Kepler conjecture official paper 2017 Forum Mathematics Pi","site:cambridge.org Flyspeck formal proof Kepler conjecture Hales 2017"],"sources":[{"source_id":"s1","title":"Computer Aided Proofs","publisher":"London Mathematical Society","url":"https://www.lms.ac.uk/publications/policies/computeraidedproofs","source_class":"OFFICIAL_GUIDANCE","publication_date":"2024-11","accessed_at":"2026-08-03","claims_supported":["The LMS is an identifiable publication authorizer for computer-aided proofs.","It requires authors to disclose the role of computation and make underpinning code and files available.","It expects transparent, surveyable code and efforts to minimize errors such as round-off error, while retaining ordinary journal review."]},{"source_id":"s2","title":"Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations","publisher":"arXiv","url":"https://arxiv.org/abs/1301.1702","source_class":"PRIMARY_RESEARCH","publication_date":"2013-01-08","accessed_at":"2026-08-03","claims_supported":["Formal verification of multivariate nonlinear inequalities on rectangular domains is technically demonstrated in HOL Light.","Flyspeck contained roughly 1,000 nonlinear inequalities, establishing a consequential real workload.","The authors reported formal verification about 2,000–4,000 times slower than an informal C++ procedure, showing a material resource constraint."]},{"source_id":"s3","title":"A Safe Computational Framework for Integer Programming applied to Chvátal's Conjecture","publisher":"arXiv","url":"https://arxiv.org/abs/1809.01572","source_class":"PRIMARY_RESEARCH","publication_date":"2018-09-05","accessed_at":"2026-08-03","claims_supported":["A rational branch-and-bound certificate and an independent checker have been used in a machine-assisted mathematical proof.","The certificate is self-contained and independently checkable rather than requiring trust in the producing solver.","VIPR encodes a branch-and-bound proof as a list of valid inequalities, providing close domain-adjacent prior art.","The work highlights both exact arithmetic and independent validation of the problem input as trust-boundary requirements."]},{"source_id":"s4","title":"Alethe: Towards a Generic SMT Proof Format","publisher":"Electronic Proceedings in Theoretical Computer Science / arXiv","url":"https://arxiv.org/abs/2107.02354","source_class":"PRIMARY_RESEARCH","publication_date":"2021-07-06","accessed_at":"2026-08-03","claims_supported":["Solver-specific proof formats and heterogeneous solver internals have impeded a shared SMT proof format.","Alethe was deliberately generalized for production by multiple solvers and reconstruction by Coq and Isabelle.","The authors describe repeated refinement, a specification, and independent tooling as necessary for multi-implementation adoption."]},{"source_id":"s5","title":"Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format","publisher":"Springer Nature","url":"https://link.springer.com/chapter/10.1007/978-3-031-30823-9_19","source_class":"PRIMARY_RESEARCH","publication_date":"2023-04-22","accessed_at":"2026-08-03","claims_supported":["Carcara demonstrates an independent checker for a proof format used by multiple SMT systems.","It distinguishes valid, holey, and invalid outcomes instead of collapsing unchecked or incomplete evidence into validity.","Its implementation includes about 6,500 lines of checking code, a 2,000-line handwritten parser, and internal normalization of step identifiers and shared terms, informing feasibility and cost scope.","The paper reports that lack of a standalone checker harmed usability and adoption of the proof format."]},{"source_id":"s6","title":"Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL","publisher":"Schloss Dagstuhl – Leibniz Center for Informatics","url":"https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/html/LIPIcs.ITP.2025.26/LIPIcs.ITP.2025.26.html","source_class":"PRIMARY_RESEARCH","publication_date":"2025","accessed_at":"2026-08-03","claims_supported":["A real proof-reconstruction implementation was found to be over-specialized to one solver's output rather than the declared Alethe standard.","The authors found tightly coupled components, insufficiently diverse tests, and an inability to test generation and reconstruction separately.","They responded with cleaner interfaces, specification clarifications, and analysis/debugging tools, directly supporting the stated problem class and workflow feasibility."]},{"source_id":"s7","title":"The Alethe Proof Format: An Evolving Specification and Reference","publisher":"veriT / LORIA","url":"https://verit.loria.fr/documentation/alethe-spec.pdf","source_class":"STANDARD","publication_date":"2023-02-17","accessed_at":"2026-08-03","claims_supported":["Alethe separates an abstract checking procedure that specifies semantics from its concrete SMT-LIB-based syntax.","The reference is intended to ensure compatibility among solvers, proof assistants, and checkers and to expose hidden implementation disagreements.","The specification remains evolving rather than immutable, demonstrating the need for version and stewardship controls."]},{"source_id":"s8","title":"A Formal Proof of the Kepler Conjecture","publisher":"Cambridge University Press","url":"https://www.cambridge.org/core/journals/forum-of-mathematics-pi/article/formal-proof-of-the-kepler-conjecture/78FBD5E1A3D1BCCB8E0D5B0C463C9FBC","source_class":"PRIMARY_RESEARCH","publication_date":"2017-05-29","accessed_at":"2026-08-03","claims_supported":["The completed Flyspeck project produced a formally checked proof using HOL Light and Isabelle.","The publication establishes theorem authors, formalization implementers, and journal reviewers as real actors around computer-assisted inequality evidence.","It demonstrates that formal verification can support a major accepted mathematical result, although it does not demonstrate the proposed representation-independent certificate contract."]}],"problem_evidence":{"support":"MODERATE","rationale":"The problem class is visible: solver-specific proof formats remain common, and an Isabelle integration was demonstrably over-specialized to one solver's output despite a nominal standard. Nonlinear inequality verification is also a real and computationally significant mathematical workload. However, no source identifies the candidate's particular unnamed audit script or verifies that its node numbers, traversal order, decimal formatting, heuristic labels, and serialization layout are acceptance-relevant. The exact local problem therefore remains an unverified instance of a well-supported general failure mode.","source_ids":["s2","s4","s6","s8"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"The LMS is an identifiable publication authorizer expressing a need for disclosed, available, transparent, surveyable computer-aided proof materials with round-off risks minimized. Flyspeck and the cited proof-format projects identify plausible authors, checker maintainers, proof-assistant developers, and reviewers. None expresses demand for this exact inequality-certificate state contract or commits to a pilot, so adopter pull is relevant but indirect.","source_ids":["s1","s4","s5","s6","s8"]},"prior_art":{"proximity":"SUBSTANTIAL_COLLISION","closest_analogues":[{"name":"VIPR-style rational branch-and-bound certificates with independent checking","similarity":"Uses exact rational branch-and-bound evidence, a self-contained certificate, and a checker independent of the solver for a machine-assisted mathematical theorem.","remaining_difference":"The published application concerns integer programming and represents the proof as valid inequalities; the searched source does not establish one semantic inequality-coverage contract accepting tree, DAG, and streamed encodings interchangeably.","source_ids":["s3"]},{"name":"Alethe proof format plus Carcara independent checker","similarity":"Defines proof semantics independently of solver internals, supports multiple producers and consumers, normalizes incidental identifiers and sharing internally, and separates valid, incomplete-with-holes, and invalid outcomes.","remaining_difference":"Alethe is a concrete SMT proof language, not a nonlinear box-coverage contract, and the sources do not show interchangeable tree and event-stream encodings of the same inequality certificate.","source_ids":["s4","s5","s7"]},{"name":"Isabelle/HOL Alethe reconstruction refactoring","similarity":"Exhibits the candidate's central symptom: nominally standard-compliant evidence was rejected or mishandled because a consumer was over-specialized to one producer, with tightly coupled components and inadequate conformance tests.","remaining_difference":"The intervention addresses an SMT-to-Isabelle reconstruction pipeline, not exact bound witnesses, rational box coverage, or a terminal empty-frontier invariant.","source_ids":["s6"]},{"name":"Flyspeck nonlinear-inequality verification in HOL Light","similarity":"Checks bounded multivariate nonlinear inequalities in a small-kernel proof-assistant setting and demonstrates consequential mathematical use.","remaining_difference":"It verifies inside HOL Light rather than exposing the proposed representation-independent certificate ADT and cross-encoding conformance suite.","source_ids":["s2","s8"]}],"distinctive_claim_remaining":"For one frozen bounded inequality, fixed trusted-lemma manifest, resource profile, and preregistered fixture corpus, an independently parsed explicit-tree certificate and an independently parsed event stream can map to the same frontier-and-coverage state contract and produce identical contract-level verdicts under node renaming, independent-branch reordering, and contract-preserving evidence sharing, while every seeded coverage loss or exact-evidence corruption is rejected. This is a local engineering claim, not a claim of a new general proof-certificate method.","confidence":"HIGH"},"implementation_evidence":{"support":"STRONG","rationale":"Exact or formally checked nonlinear inequality verification, rational branch-and-bound certificates, independent proof checkers, semantic proof-format specifications, multi-producer integrations, and representation normalization have all been implemented. Carcara's code-scale disclosure and Flyspeck's performance results show that the work is feasible but nontrivial. The offline/no-network design poses little data or privacy risk. Scholarly acceptance remains with authors and journals; the contract cannot confer that authority. The unverified elements are the candidate's actual adapters, the exact kernel and lemma manifest, ambiguity-free abstraction maps, corpus representativeness, and performance on the intended artifacts.","source_ids":["s1","s2","s3","s5","s6","s7","s8"]},"scores":{"meaningful_impact":{"score":3,"rationale":"If the stated coupling exists, separating mathematical obligations from generator traces could improve preservation, independent audit, and safe implementation replacement. The proposed pilot covers one inequality and does not yet show reduced errors, review time, or long-term preservation outcomes.","source_ids":["s1","s2","s6","s8"]},"stakeholder_pull":{"score":3,"rationale":"Publication policy and existing formal-proof projects show demand for transparent, independently checkable evidence, but no named stakeholder has requested or committed to this particular contract.","source_ids":["s1","s5","s8"]},"incremental_advantage":{"score":3,"rationale":"A semantic state contract could avoid frozen stacks and pairwise converters, but its advantage over one canonical certificate format or direct proof-assistant checking has not been measured.","source_ids":["s3","s4","s7"]},"distinctiveness_plausibility":{"score":2,"rationale":"Generic proof formats, exact branch-and-bound certificates, independent checkers, semantic checking procedures, and refactoring away from producer-specific output substantially collide with the mechanism. Only the inequality-specific, cross-representation coverage contract remains plausibly distinctive.","source_ids":["s3","s4","s5","s6","s7"]},"technical_implementability":{"score":4,"rationale":"All major technical ingredients have credible precedents, including exact arithmetic, branch-and-bound certificates, standalone checkers, semantic rules, and independent parsers. Performance and abstraction-map ambiguity are the principal open technical risks.","source_ids":["s2","s3","s5","s7"]},"adoption_authority_feasibility":{"score":4,"rationale":"The authors and kernel maintainers can authorize an isolated offline pilot, while journals retain acceptance authority. LMS policy is compatible with transparent, surveyable checking, but no publisher endorsement of this format is implied.","source_ids":["s1","s8"]},"evidence_readiness":{"score":2,"rationale":"The proposal supplies a concrete experimental design but no named pipeline, dependency inventory, certificate artifacts, adapters, results, stakeholder commitment, or measured resource use.","source_ids":["s5","s6"]},"safety_net_benefit":{"score":4,"rationale":"Exact checking, independent verification, explicit non-success outcomes, seeded corruptions, and retention of the incumbent verifier could provide a strong reversible safety layer. Shared-kernel or input errors remain possible.","source_ids":["s1","s3","s5"]},"scalability":{"score":3,"rationale":"Multi-solver proof formats and standalone checking demonstrate architectural scalability, but formal nonlinear verification can be orders of magnitude slower than informal computation and format integrations require substantial tooling and diverse tests.","source_ids":["s2","s4","s5","s6"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"Inventory one actual verifier's acceptance-relevant dependencies, specify the abstract state and trust boundary, freeze 24 fixtures and falsifiers, and obtain pilot authorization.","confidence":"LOW","assumptions":["Approximately 3–8 expert person-weeks at blended 2026 research-software and formal-methods labor rates.","The existing certificate, verifier, and generator are accessible and documented enough for dependency tracing.","No publication-grade soundness proof is included."],"source_ids":["s1","s5","s6"]},"initial_deployment_startup":{"band_2026_usd":"50K_TO_250K","scope":"Implement the explicit-tree verifier, independently parsed event-stream adapter, abstract checker, metamorphic/property tests, seeded mutants, and reproducible offline runner.","confidence":"LOW","assumptions":["Approximately 3–9 expert person-months.","The inequality language and trusted-lemma manifest are bounded.","No shared parsing code is used between the two representations.","The estimate is resource-equivalent, not a vendor quote."],"source_ids":["s2","s3","s5"]},"operational_launch":{"band_2026_usd":"50K_TO_250K","scope":"Harden parsers and resource limits, perform independent mathematical and security review, integrate CI and archival packaging, document versioning, and execute the preregistered pilot.","confidence":"LOW","assumptions":["One bounded proof pipeline rather than an ecosystem-wide standard.","Existing institutional compute and repository infrastructure are available.","Publication acceptance remains a separate reviewer decision.","Exact checking does not require large dedicated hardware."],"source_ids":["s1","s2","s5","s7"]},"annual_recurring":{"band_2026_usd":"10K_TO_50K","scope":"Maintain contract versions, fixtures, adapters, dependencies, archival builds, CI checks, and periodic trust-boundary review.","confidence":"LOW","assumptions":["Approximately 0.1–0.3 expert FTE plus modest compute and storage.","Few contract revisions and at most a small number of maintained representations per year.","Legacy versions are bounded by an explicit support policy."],"source_ids":["s1","s6","s7"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"YES","reason":"Published evidence shows both a consequential nonlinear-inequality verification workload and the general failure mode of a proof consumer being over-specialized to one producer's output. The exact unnamed pipeline remains unverified, limiting support to the problem class.","source_ids":["s2","s4","s6"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"The London Mathematical Society is an identifiable publication authorizer with an explicit policy requiring transparent, surveyable, available computer-aided proof materials. This establishes relevant authority and need, not commitment to adopt the proposed contract.","source_ids":["s1"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The tree-versus-event-stream verdict-equivalence claim is contrastive and falsifiable against the incumbent checker, a direct exact model checker, metamorphic representation changes, and seeded invalid certificates.","source_ids":["s3","s5","s6"]},"bounded_next_evidence_step":{"status":"YES","reason":"One claim, 24 frozen fixtures, two independently parsed representations, one abstract checker, fixed resources, predetermined transformations, and explicit halt conditions form a bounded pilot.","source_ids":["s3","s5","s6"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The proposed first step is offline, reversible, non-publication-gating, retains the original verifier, separates non-success outcomes, and leaves proof acceptance with authors and reviewers. Kernel soundness still requires examination during the pilot.","source_ids":["s1","s3","s5"]},"credible_cost_scope_and_range":{"status":"UNCERTAIN","reason":"Comparable checker scale and formal-verification performance bound the order of work, but no actual codebase, artifact size, staffing plan, labor rate, or compute benchmark was supplied. The bands are planning estimates only.","source_ids":["s2","s5","s6"]}},"next_evidence_step":"Secure access and written authorization for one actual, non-publication-gating inequality-certificate pipeline. Before implementation, freeze the claim, rational domain, trusted-lemma manifest, contract version, hardware-neutral resource profile, incumbent checker, direct exact model checker, and 24 fixtures spanning valid, incomplete, malformed, omitted-child, overlap, degenerate-split, corrupted-bound, unknown-lemma, reordered-branch, renamed-node, and evidence-sharing cases. Independently implement an explicit-tree reader and event-stream reader with no shared parser, map both into the same state checker, and compare both against the incumbent and direct model checker. Preregister wall-time and memory ceilings. Falsify the claim if either abstraction map is ambiguous, any seeded coverage or evidence defect reaches Verified, any representation-only transformation changes a contract-level verdict, any non-success outcome is promoted to Verified, or the valid corpus cannot be checked within the resource ceilings. Preserve every disagreement and do not relax the contract after observing results.","blocking_evidence":["No externally inspected dependency inventory shows that the stated node-numbering, traversal-order, formatting, heuristic, or serialization dependencies exist in the intended verifier.","No named theorem author, kernel maintainer, repository custodian, or publication reviewer has committed to the pilot.","No actual certificate corpus or independent tree/event-stream implementations have been tested.","No empirical evidence establishes verdict equivalence, seeded-defect rejection, parser independence, or resource performance.","The trusted arithmetic kernel, lemma manifest, input validation, and contract-version migration rules have not been independently audited.","Cost bands lack measured person-hours, artifact sizes, compute requirements, and maintenance history."],"research_disposition":"PARTNERED_RESEARCH_PROGRAM","world_novelty_boundary":"World novelty, patentability, freedom to operate, market size, and realized impact were not measured. The eight-source search found substantial prior art for exact rational branch-and-bound certificates, generic semantic proof formats, independent checkers, multi-producer compatibility, and refactoring consumers away from producer-specific output. It did not establish whether an inequality-specific frontier-and-coverage contract supporting interchangeable tree, DAG, and stream representations has or has not been implemented elsewhere; no novelty claim is supportable.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Name and inspect the actual generator, certificate artifact, verifier, kernel maintainer, and publication authority.","Produce an acceptance-dependency inventory distinguishing mathematical obligations from incidental representation fields.","Obtain written authorization for the isolated non-publication-gating pilot and define who may approve trust-boundary changes.","Freeze the 24-fixture corpus, comparators, transformations, failure categories, contract version, and resource ceilings before coding.","Implement independent tree and event-stream paths and publish all verdict comparisons, mutation results, disagreements, and resource measurements.","Independently review the exact-arithmetic kernel, trusted-lemma manifest, input validation, and rollback path.","Record actual person-hours, compute use, and maintenance requirements to replace the provisional cost bands."],"reason":"Bounded web research establishes the problem class, relevant authority, strong technical feasibility, and substantial prior-art collision, but it cannot determine whether the unnamed target pipeline has the asserted dependencies or whether the remaining tree-versus-stream claim holds. Those questions require access to artifacts, implementation work, mutation testing, and measured execution; therefore the next decision depends on empirical research rather than further bounded web search."},"proposal_index":3}