On this page
Formal theorem coverage auditor
Edition: 8 October 2026. Initial decision: Prototype now. The product interpretation and pricing are hypotheses; independent proof and buyer validation remain open.
Research finding
Several scope documents distinguish a paper's claim from the selected formal statement. Family 131 excludes the exact sampler; family 149's formal scope concerns an older boundedness result; family 276 excludes arbitrary partner-channel additivity and separate-measurement decoding.
Problem and buyer
A technical reviewer may read 'formalized' as coverage of every headline, algorithmic complexity assertion and corollary. Research labs, publishers and engineering due-diligence teams need a precise record of what a checked statement would support.
What the finding could enable
An assumption and coverage map can align natural-language claims, formal definitions and implementation assertions. A CI linter can catch later marketing or documentation claims that exceed approved coverage, with a human review workflow for semantic ambiguity.
Technical and commercial limits
Text similarity cannot establish theorem equivalence. The system must show source evidence and separate automated suggestions from reviewed mappings. Static flags such as 'outside' are diagnostics, not proof failures.
Minimal architecture
Manuscript claim extraction -> formal-statement index -> proposed alignment -> reviewer approval -> documentation linter. Pair each record with assumptions, output guarantee, cost model and formalization edition.
Existing alternatives and differentiation
Comparator checks selected theorem equivalence and allowed axioms. This product addresses the layer between a selected theorem and a paper or product claim. Existing review checklists and project maintainers are the main practical substitutes.
Monetization hypothesis
Hypothesis: AUD 3,000-10,000 per bounded claim audit, with a later team subscription. A services-first approach tests whether semantic review can be standardized enough to sustain a software margin.
Validation experiment
Create twenty manually labeled claim-to-statement pairs, including the identified exclusions, then measure both unsupported approvals and unnecessary escalations. Require zero automated assertions of complete coverage.
Conditions to reject or defer
Defer if every case needs expensive specialist interpretation and customers cannot fund that work, or if the tool repeatedly treats paper-version drift as a mathematical contradiction.
Next concrete action
Create the first twenty coverage records with source passages, selected statement names and specific exclusions.
Source evidence
Repository sources are pinned to revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Selected scope notes and manuscript statements have been reviewed to the extent described above; these links do not represent successful kernel checks.
Family 104
Subject: Quasipolynomial algorithms for mean-payoff, stochastic and parity games.
- Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time
- Mean-payoff parity games in quasipolynomial time
- Deterministic quasipolynomial-time mean-payoff games
- Randomized quasipolynomial-time mean-payoff games
- Formal scope notes
Family 107
Subject: Matrix multiplication with exponent at most 9/4.
- An Upper Bound of 9/4 for the Matrix Multiplication Exponent
- Complex Matrix Multiplication Below 2.258 and Rectangular Bounds
- Staggered extraction for exact matrix multiplication over every field
- Formal scope notes
Family 131
Subject: Rapid mixing of graph switches for every degree sequence.
Family 149
Subject: Classwise permanence for weakly reversible mass-action systems.
- Uniform Permanence in Weakly Reversible Mass-Action Systems
- Boundedness and persistence of weakly reversible mass-action systems
- Formal scope notes
Family 276
Subject: Classical capacity of generalized amplitude damping.
Current alternative sources
Primary documentation reviewed on 8 October 2026. Product availability demonstrates alternatives, not demand or willingness to pay for this proposal.