{"schema_version":1,"research_id":"eoa_inverse_innovation_exp06_external_evaluation_20260803","source_assessment_id":"predictive_residual_processing__mathematics:P1:v0","cell_id":"predictive_residual_processing__mathematics","search_queries":["Lean 4 proof state InfoTree documentation goals messages official","proof assistant proof state visualization large proofs review cognitive load research","Alectryon proof state diffs documentation","Coq SerAPI proof states protocol paper","QED at Large survey engineering formally verified software proof maintenance PDF","formal proof engineering large developments maintenance proof state visualization paper","Lean proof state diff highlighting goals changed Infoview official","Alectryon proof state snapshots official documentation","empirical study proof assistant user experience proof state interface goals usability","Lean Infoview performance large proof state issue official","proof state diff theorem prover IDE research paper","incremental proof state document model Isabelle PIDE official paper","mathlib pull request review maintainers official documentation Lean","Lean 4 plugin InfoView extension official documentation widgets","Lean 4 InfoTree documentation official elaboration info","Lean proof state diff goals highlighting implementation","site:bls.gov/ooh computer and information technology software developers median pay 2025","site:bls.gov/oes software developers May 2025 wage","QED in Context observation study proof assistant users PDF 2025 ACM","Untangling formal proofs Alectryon paper official"],"sources":[{"source_id":"S1","title":"QED in Context: An Observation Study of Proof Assistant Users","publisher":"Proceedings of the ACM on Programming Languages / University at Buffalo research portal","url":"https://researchconnect.buffalo.edu/en/publications/qed-in-context-an-observation-study-of-proof-assistant-users/","source_class":"PRIMARY_RESEARCH","publication_date":"2025-04-09","accessed_at":"2026-08-03","claims_supported":["A contextual-inquiry study observed 30 Rocq and Lean users.","Even experts find proof assistants challenging to use effectively.","Proof writers repeatedly react to prover feedback and have challenging interactions with the assistant, supporting a usability and attention problem, though not specifically a transcript-volume problem."]},{"source_id":"S2","title":"Roadmap","publisher":"Mathlib Initiative","url":"https://mathlib-initiative.org/roadmap/","source_class":"OFFICIAL_ORGANIZATION_DATA","publication_date":"2026","accessed_at":"2026-08-03","claims_supported":["The Mathlib Initiative calls the review-queue bottleneck the primary constraint on Mathlib growth.","It reports roughly 300 waiting pull requests and median waits around two weeks.","It plans professional review capacity and automation to reduce manual review overhead, identifying a plausible funder and adopter with expressed need for review tooling."]},{"source_id":"S3","title":"Pull Request Review Guide","publisher":"Lean Prover Community / Mathlib","url":"https://leanprover-community.github.io/contribute/pr-review.html","source_class":"OFFICIAL_GUIDANCE","publication_date":"n.d. (live guidance accessed 2026-08-03)","accessed_at":"2026-08-03","claims_supported":["Mathlib maintainers alone have authority to merge pull requests.","Reviewers and maintainers are identifiable workflow participants for a read-only evaluation.","Deployment into authoritative review would require maintainer approval."]},{"source_id":"S4","title":"Lean 4 VS Code Extension Manual","publisher":"Lean Prover","url":"https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"n.d. (live documentation accessed 2026-08-03)","accessed_at":"2026-08-03","claims_supported":["Lean's InfoView already shows current proof states, goals, expected types, and diagnostics.","It already highlights changed portions of proof states in red and green, creating a substantial prior-art collision with residual-focused presentation.","InfoView supports pinning, pausing, collapsing, searching traces, and extensible user widgets, making a side-by-side prototype technically plausible."]},{"source_id":"S5","title":"Lean.Elab.InfoTree.Types","publisher":"Lean Prover","url":"https://lean-lang.org/doc/api/Lean/Elab/InfoTree/Types.html","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","publication_date":"n.d. (live API documentation accessed 2026-08-03)","accessed_at":"2026-08-03","claims_supported":["Lean generates an InfoTree during elaboration for language-server access to tactic and expected-type information.","InfoTree nodes retain syntax mapping and local contexts, and goalsAt can retrieve tactic information.","The API supplies much of the structured data needed for an offline proof-state recorder, while holes and asynchronous completion complicate canonical snapshots."]},{"source_id":"S6","title":"Interaction with Formal Mathematical Documents in Isabelle/PIDE","publisher":"arXiv; Makarius Wenzel","url":"https://arxiv.org/abs/1905.01735","source_class":"PRIMARY_RESEARCH","publication_date":"2019-05-05","accessed_at":"2026-08-03","claims_supported":["Isabelle/PIDE is an established prover IDE using an asynchronous document model and parallel evaluation.","It demonstrates mature incremental processing and semantic presentation of formal mathematical documents.","It is adjacent prior art for versioned, incremental proof-state interaction, but does not establish the proposed residual codec, exact reconstruction, raw audits, or safety bypass."]},{"source_id":"S7","title":"Untangling Formal Proofs","publisher":"ACM SLE / Massachusetts Institute of Technology author-hosted copy","url":"https://people.csail.mit.edu/cpitcla/links/2020-08-05-alectryon.pdf","source_class":"PRIMARY_RESEARCH","publication_date":"2020","accessed_at":"2026-08-03","claims_supported":["Alectryon reports that nontrivial proof scripts are hard to understand because scripts record steps rather than resulting states.","It identifies manual proof-state snapshots as cumbersome, error-prone, fragile, and vulnerable to staleness after prover or library updates.","Alectryon records prover goals and responses and interleaves them with scripts in interactive documents, closely overlapping the transcript and review-presentation portions of the proposal."]},{"source_id":"S8","title":"Software Developers, Quality Assurance Analysts, and Testers","publisher":"U.S. Bureau of Labor Statistics","url":"https://www.bls.gov/ooh/computer-and-information-technology/software-developers.htm","source_class":"GOVERNMENT_OR_REGULATOR","publication_date":"2025-08-28","accessed_at":"2026-08-03","claims_supported":["The May 2024 median annual wage was $133,080 for software developers and $102,610 for software quality-assurance analysts and testers.","These wages provide an official labor anchor for 2026 resource-equivalent cost bands, subject to inflation, benefits, overhead, and specialist-proof-engineer premiums."]}],"problem_evidence":{"support":"MODERATE","rationale":"The problem is visible at two levels: a primary user study finds difficult, feedback-intensive proof-assistant work, and Alectryon documents the incomprehensibility and staleness problems surrounding proof-state presentation. Mathlib officially reports a material review bottleneck. However, no source measures the candidate's specific predicates—complete proof-state transcript volume, repeated-content fraction, reviewer time spent on unchanged state, or missed consequential state changes—so prevalence and magnitude remain unverified.","source_ids":["S1","S2","S7"]},"stakeholder_evidence":{"support":"MODERATE","rationale":"Mathlib maintainers are identifiable authorizers, and the Mathlib Initiative explicitly seeks review automation and funds professional review capacity. This establishes credible authority and adjacent pull, but neither organization expressly requests predictive residual proof-state transcripts. Interest in the exact intervention must be confirmed before integration.","source_ids":["S2","S3"]},"prior_art":{"proximity":"SUBSTANTIAL_COLLISION","closest_analogues":[{"name":"Lean InfoView proof-state change highlighting","similarity":"Already presents goals and diagnostics and highlights inserted or removed portions of a changing proof state, directly addressing the residual-attention concept in the proposal.","remaining_difference":"The manual does not describe an archived, reconstructible residual transcript with predictor/environment fingerprints, canonical digests, independent raw sampling, protected-event bypasses, or automatic full-state fallback.","source_ids":["S4"]},{"name":"Alectryon recorded proof-state documents","similarity":"Records goals and prover responses and interleaves them with proof scripts for interactive review without rerunning the proof; it also addresses stale, fragile proof-state snapshots.","remaining_difference":"Alectryon presents recorded outputs rather than making prediction-relative structured residuals the primary message, and the paper does not establish exact residual reconstruction, consequence gating, raw-channel audits, or automatic decompression.","source_ids":["S7"]},{"name":"Isabelle/PIDE incremental document interaction","similarity":"Provides an established incremental, asynchronous prover-document model with semantic feedback and version-sensitive processing.","remaining_difference":"Its primary concern is responsive document processing, not residual-only proof-state transcripts, exact reconstruction from predictor plus delta, or safety-governed suppression.","source_ids":["S6"]},{"name":"Lean InfoTree and user-widget infrastructure","similarity":"Exposes structured tactic, context, syntax, and goal information and permits custom InfoView components, supplying much of the implementation substrate.","remaining_difference":"Infrastructure is not evidence that the coupled residual codec, audit protocol, and reviewer workflow already exist or improve outcomes.","source_ids":["S4","S5"]}],"distinctive_claim_remaining":"On a preregistered archived Lean corpus, a version-gated one-step proof-state predictor plus structured residual view will reduce stored/displayed transcript bytes by at least 40% and median reviewer task time by at least 20% versus both complete-state review and Lean's existing change highlighting, while achieving 100% canonical reconstruction on audited states, zero omissions of blinded protected changes, and lower total prediction-plus-audit cost than the full-state baseline. These thresholds are proposed falsifiers, not established effects.","confidence":"HIGH"},"implementation_evidence":{"support":"MODERATE","rationale":"Lean already exposes structured proof-state information through InfoTree, highlights state changes, and supports custom InfoView widgets. Alectryon proves that prover responses can be captured into replayable documents, while Isabelle/PIDE demonstrates mature incremental interaction. An offline, read-only prototype is therefore credible. Remaining hard problems are stable canonicalization across elaborator/library versions, treatment of asynchronous InfoTree holes, dependency and trust-boundary extraction, deterministic replay, exact digest semantics, confidentiality of unusual residuals, and reliable fallback testing. No external source validates the complete coupled architecture.","source_ids":["S4","S5","S6","S7"]},"scores":{"meaningful_impact":{"score":3,"rationale":"Formal-proof usability and Mathlib review capacity matter, but the share attributable to repeated proof-state content and the achievable time reduction are unmeasured.","source_ids":["S1","S2","S7"]},"stakeholder_pull":{"score":3,"rationale":"Mathlib has explicit pull for reducing review overhead and clear maintainers, but no expressed demand for this specific residual transcript.","source_ids":["S2","S3"]},"incremental_advantage":{"score":2,"rationale":"Lean already highlights proof-state changes and Alectryon already records interactive proof-state documents; added value depends on whether prediction, reconstruction, audits, and fallback outperform these simpler approaches.","source_ids":["S4","S7"]},"distinctiveness_plausibility":{"score":3,"rationale":"The coupled safety-governed, reconstructible residual architecture remains distinguishable, although its visible-review core substantially collides with existing tools.","source_ids":["S4","S6","S7"]},"technical_implementability":{"score":4,"rationale":"Official Lean APIs and widgets make an offline prototype feasible; cross-version canonicalization and protected dependency extraction remain material engineering uncertainties.","source_ids":["S4","S5","S7"]},"adoption_authority_feasibility":{"score":3,"rationale":"Mathlib maintainers have clear authority and a side-by-side read-only study avoids changing theorem acceptance, but partnership and eventual workflow approval are not secured.","source_ids":["S2","S3"]},"evidence_readiness":{"score":4,"rationale":"Open archived corpora, existing full-state behavior, structured Lean APIs, and explicit comparators permit a bounded preregistered replay and reviewer study.","source_ids":["S3","S4","S5"]},"safety_net_benefit":{"score":4,"rationale":"Keeping kernel acceptance unchanged, retaining protected events in full, auditing raw states, and reverting to complete transcripts can sharply bound pilot risk; the reliability of these controls still requires adversarial testing.","source_ids":["S3","S4","S5"]},"scalability":{"score":3,"rationale":"Incremental prover infrastructure scales in established systems, but predictor maintenance, anchoring, raw audits, version churn, and frequent fallback could erase savings on heterogeneous libraries.","source_ids":["S5","S6","S7"]}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"10K_TO_50K","scope":"Preregister and execute an offline replay on one fixed public archived corpus; build a minimal extractor and canonical comparator; compare full states, existing Lean change highlighting, and residual views; recruit a small reviewer sample; report bytes, reconstruction, protected-change recall, task time, compute, and fallback.","confidence":"MODERATE","assumptions":["Roughly 200-450 specialist engineering and research hours.","Public corpus avoids licensing and data-acquisition expense.","Existing Lean APIs and UI components are reused.","Reviewer honoraria and modest compute are included.","BLS wages are uplifted for benefits, overhead, inflation to 2026, and proof-assistant specialization."],"source_ids":["S4","S5","S8"]},"initial_deployment_startup":{"band_2026_usd":"50K_TO_250K","scope":"Develop a robust read-only prototype with version fingerprints, structured canonicalization, replay storage, protected-event rules, raw audit sampling, full-state anchors, fallback, and a usable reviewer interface.","confidence":"MODERATE","assumptions":["Approximately 0.5-1.5 loaded specialist FTE-years.","No modification to the Lean kernel or theorem-acceptance path.","One prover and one repository workflow are supported initially.","Security review is limited to archived or public proofs."],"source_ids":["S4","S5","S8"]},"operational_launch":{"band_2026_usd":"250K_TO_1M","scope":"Productionize for a large collaborative repository with CI integration, deterministic retention, access controls, observability, adversarial protected-event tests, documentation, maintainer governance, migration support, and incident rollback.","confidence":"LOW","assumptions":["Approximately 2-5 loaded FTE-years across proof engineering, product/UI, QA, security, and repository operations.","Launch follows a successful read-only trial and explicit maintainer authorization.","Private or embargoed proof content may require additional controls.","Existing complete-state and kernel-checking paths remain available."],"source_ids":["S2","S3","S4","S8"]},"annual_recurring":{"band_2026_usd":"50K_TO_250K","scope":"Maintain canonicalizers and predictors across Lean and library releases; operate audits, storage, monitoring, fallback drills, regression corpora, and reviewer support.","confidence":"LOW","assumptions":["Approximately 0.5-1.5 loaded FTE-years plus modest compute and storage.","Scope remains one prover ecosystem.","Frequent version churn or fallback could move costs above this band.","Canonical full transcripts continue to be retained under repository policy until evidence supports any retention change."],"source_ids":["S2","S5","S8"]}},"verified_pipeline_gates":{"externally_supported_problem":{"status":"YES","reason":"Primary research and prior-art papers establish difficult feedback-intensive proof work and proof-state comprehensibility/staleness problems; Mathlib reports a consequential review bottleneck. The specific transcript-redundancy prevalence remains a measurement gap but does not erase the broader problem.","source_ids":["S1","S2","S7"]},"externally_credible_adopter_or_authorizer":{"status":"YES","reason":"Mathlib maintainers are the documented merge authorities, and the Mathlib Initiative is actively resourcing review automation and reduced manual overhead.","source_ids":["S2","S3"]},"distinct_testable_incremental_claim":{"status":"YES","reason":"The remaining claim can be tested against complete-state review, current Lean change highlighting, and an Alectryon-style recorded-state view using explicit byte, time, reconstruction, protected-change, fallback, and total-cost outcomes.","source_ids":["S4","S7"]},"bounded_next_evidence_step":{"status":"YES","reason":"A fixed archived corpus, untouched holdout, side-by-side replay, blinded protected changes, and bounded reviewer tasks form a finite evidence step that changes no proof acceptance or canonical artifact.","source_ids":["S3","S4","S5"]},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The first step is read-only and offline; the kernel and maintainers retain their existing authority, and any mismatch can revert immediately to unchanged complete transcripts. Private-data use and operational suppression remain outside the authorized scope.","source_ids":["S3","S4"]},"credible_cost_scope_and_range":{"status":"YES","reason":"All four bands are tied to explicit FTE, integration, governance, compute, and retention assumptions and anchored to official software-development and QA wages; production estimates remain low-confidence.","source_ids":["S8"]}},"next_evidence_step":"Partner with one Lean/Mathlib maintainer and preregister an 8-12 week, read-only study on one frozen public corpus plus an untouched holdout. Randomize at least 20 qualified reviewers across four conditions: complete proof states, current Lean InfoView change highlighting, an Alectryon-style recorded-state view, and the proposed version-gated residual view. Blindly insert protected axiom/dependency/obligation/error changes. Measure canonical reconstruction, protected-change recall, false suppression, task accuracy and time, transcript bytes, compute, audit effort, fallback frequency, and total resource cost. Falsify authorization if any protected event is omitted, any audited state fails exact canonical reconstruction, silence masks missing output or version mismatch, median task time improves by less than 20%, bytes improve by less than 40%, task accuracy falls, or total cost is not below the full-state comparator. A passing result licenses only a larger read-only replication.","blocking_evidence":["No external measurement establishes the repeated-content fraction or storage burden of complete proof-state transcripts in a representative large corpus.","No comparative study shows that residual presentation improves reviewer time or accuracy beyond Lean's existing red/green proof-state highlighting.","The exact overlap with unpublished, repository-local, or plugin-based proof-state diff and transcript tools remains unknown.","Stable canonical representations for names, ordering, contexts, dependencies, warnings, and asynchronous InfoTree holes have not been demonstrated across Lean/library versions.","Zero-omission performance for rare protected changes and reliable automatic fallback have not been live-tested.","Mathlib maintainer interest in this exact intervention and willingness to host a reviewer study are unconfirmed.","Confidentiality and retention rules for private or embargoed formalizations have not been evaluated.","Net savings after prediction, metadata, anchors, raw audits, reviewer retraining, and maintenance are unmeasured."],"research_disposition":"PARTNERED_RESEARCH_PROGRAM","world_novelty_boundary":"World novelty, patentability, freedom to operate, market size, and realized impact were not measured. The search establishes substantial collision with Lean InfoView change highlighting, Alectryon proof-state recording, and Isabelle/PIDE incremental interaction, but does not establish whether the complete safety-governed architecture has or has not appeared elsewhere.","arm":"COMPLETE_PROPOSAL_PORTFOLIO","candidate_version":0,"controller_recommendation":{"action":"STOP_EMPIRICAL_RESEARCH_NEEDED","repairable":false,"material_progress_observed":true,"progress_targets":["Quantify proof-state regularity, full-transcript bytes, and baseline reviewer navigation time on a frozen corpus and untouched holdout.","Complete a feature-level prior-art matrix against Lean InfoView, Alectryon, Isabelle/PIDE, and any repository-local plugins before claiming incremental value.","Demonstrate deterministic canonicalization and 100% audited reconstruction across supported command classes and pinned environment versions.","Show zero omissions on blinded protected axiom, dependency, obligation, trust-boundary, missing-output, and checker-error changes.","Beat both complete-state review and existing Lean change highlighting on preregistered reviewer accuracy/time thresholds without increasing total resource cost.","Obtain written maintainer approval for any study involving repository reviewers and separately authorize any move beyond read-only operation.","Document confidentiality, retention, access-control, rollback, and incident-response rules before using nonpublic proof material."],"reason":"Bounded web research found a real adjacent problem, credible authorizers, feasible implementation substrates, and substantial prior-art collision. The decisive questions—regularity, reviewer benefit over existing highlighting, exact reconstruction, protected-event recall, fallback reliability, and net cost—require corpus replay and human reviewer testing rather than further web search. Under the evaluation rule, that requires STOP_EMPIRICAL_RESEARCH_NEEDED; all STOP actions are non-repairable within this web-only evaluation."},"proposal_index":1}