28 Open theorem program
On this page · Permalink · Source line 2314
The finite protected-extension, semantic-cover, and attained-decoder problems developed in this edition are closed under their stated hypotheses. The questions below concern stronger interfaces. In particular, the rule transport sends one source rule to one target rule and is not asserted to be a general equivalence of proof fields. A transport into a derived target proof, executable correctness of the producers, and richer semantic objects remain distinct next steps.
Problem 28.1: Proof-path view functors and comparison
The declared-field local-model functor and whole-support gluing are established here. Extend the checked interface to richer proof-state representations, and verify the implementation of general proof assistant adapters. Determine when objects with symmetry require nonabelian or higher descent rather than the strict set-valued construction.
Problem 28.2: Counterfactual proof-search observations
Study which observations on a finite realization fiber yield the greatest task-relative reduction of uncertainty per unit cost. Extend the binary rank theorem to controlled infinite or nonlinear settings only after specifying distributions, admissible questions, and the semantics of proof state.
Problem 28.3: Collective evaluation without shared-context confounding
Design preregistered evaluations of identical certified mathematics under randomized labels and alternative explanatory contexts. Separate measurement of interpretation differences from independent verification of correctness, and test whether models of correlated review predict actual audit errors.
Further directions include the following problems.
Problem 28.4: Infinite proof fields
Develop locally finite and countable proof fields with conditions guaranteeing that finite certificates approximate an infinite derivation without losing domain or convergence information.
Problem 28.5: Parameterized certificate complexity
Classify minimum certificate selection by treewidth, number of alternative justifications, justification arity, shared-subproof width, and target count. Identify fixed-parameter tractable regimes and approximation bounds.
Problem 28.6: Probabilistic bridge calibration
Replace declared bridge weights by calibrated posterior models while keeping conjectural reach separate from certified derivability.
Problem 28.7: Proof assistant interoperability
Construct adapters that export stable claim identifiers, primitive dependencies, scopes, and proof terms from existing formal systems into the common proof-field schema.
Problem 28.8: Higher proof transformations
Model transformations between proofs, transformations between transformations, and coherent compiler pipelines in a higher categorical setting.
Problem 28.9: Privacy and attribution
Design proof archives that preserve provenance and priority while allowing private notes, embargoed routes, and sensitive collaboration records to remain access controlled.
Problem 28.10: Empirical validation
Study real mathematical projects to estimate recovery costs, audit bottlenecks, and the predictive value of bridge-retention scores. Such work should test the models rather than assume them.
Problem 28.11: Distributed audit systems
Extend the queue model to heterogeneous reviewers, dependent tasks, rework, priority classes, and claims whose audit cost changes after neighboring claims are resolved.