The shortest version: probability is not being used to make a theorem “probably true.” It is being used to prove that the set of valid witnesses cannot be empty. Once nonemptiness is established exactly, the conclusion is ordinary mathematics.
The distinction matters for AI-assisted reasoning. A model can be excellent at suggesting examples, decompositions, or promising regions of a search space. None of that should let the model certify its own work.
The intuition
A jar of witnesses.
Imagine a sealed jar containing possible solutions to a problem. Most slips may be wrong. A red slip is a valid witness: an assignment satisfying a formula, a combinatorial object with the required property, or a proof object accepted by a checker.
If you can prove exactly that red slips occupy any positive fraction of the jar, the jar contains at least one red slip. You do not need to draw it first. The probability calculation has established nonemptiness.
The exact mass can be tiny. Its logical consequence is still binary: empty or nonempty.
This is the classical probabilistic method. SWC does not claim to invent that implication. Its proposed contribution is an explicit, compositional certificate language and trust boundary for automated reasoning systems.
The architecture
Search is not certification.
A learned generator may concentrate probability around useful witnesses. That can make discovery dramatically easier. But a generator can also overfit, collapse onto the wrong region, or assign zero probability to an exceptional case.
Useful for hypotheses, partitions, candidate witnesses, and search priorities.
Verifier soundness, normalization, accepted mass, and the final logical status.
The v4.1 integrated SAT study makes that separation concrete. Across 60 planted satisfiable instances, the learned proposal raised median exact witness mass from 1/65,536 to 0.9393. A mixture retaining 10% uniform support produced a median 27,809.8× increase while preserving a theorem-level floor.
The result is not “the model proved SAT.” The model reshaped search. Exact rational recomputation established the accepted mass, and all 20 contradictory controls received exactly zero.
The quantifier trap
Zero hits can lie.
If a valid witness is rare, a large sample may miss it completely. That observation is compatible with both an empty witness set and a nonempty one. Sampling alone cannot distinguish the two.
How likely is a search to see nothing?
A search can miss every witness even though the true accepted mass is positive.
| Scenario | Search budget | Probability of a misleading zero |
|---|---|---|
| One exception among 10⁶ instances | 10⁴ checks | 99.00% |
| True witness mass 10⁻⁶ | 10⁵ samples | 90.48% |
(1 − δ)ⁿ for the selected witness mass and sample count. The highlighted default reproduces the manuscript’s quantifier-audit checkpoint.This is why SWC insists on pointwise quantifiers and exact lower bounds. “We tested many cases” and “we sampled no counterexample” are observations. They are not universal theorems.
The evidence
Six tests of the boundary.
The experiments do not combine into one performance score. Each probes a different failure mode or implementation layer.
- 01 · Learned SAT proposal60 satisfiable / 20 contradictory controls
Exact mass rises sharply while the uniform mixture protects support.
- 02 · Structured model countingWitness space 2²⁰⁴⁸ · about 1.1 seconds
A dynamic program certifies exact mass without enumerating the full space.
- 03 · Quantifier audit99.00% and 90.48% miss probabilities
Large-looking test budgets can still miss a single exception or rare witness mass.
- 04 · Erdős–Straus case study82,887 / 82,887 declared primes exactly proved
Every prime p ≡ 1 mod 24 below 10⁷ receives an exact witness using shifts c ≤ 127. This is a genuine finite-domain theorem; universal closure requires a further exact all-instance certificate.
- 05 · Certificate integrity300 accepted · 1,800 altered variants rejected
The checker accepts exact certificates and rejects the declared tampering and floating-point-only suite.
- 06 · Optional stopping30.826% naive · 4.342% e-process
Repeated nominal testing inflates false certification; the anytime-valid process stays within its declared 5% risk budget in simulation.
The status system
Two honest endpoints.
SWC uses one architecture but refuses to give mathematics and physical evidence the same label.
Deterministic theorem
A sound verifier plus an exact positive-mass certificate proves that a valid witness exists.
Truth is not weakened to probability.Calibrated evidence
An e-process or confidence sequence controls error under explicit assumptions and adaptive monitoring.
The conclusion remains model-conditional.The distinction is the heart of the paper. Probability inside a proof, randomized proof search, and statistical evidence about nature are related—but they are not interchangeable.
Every base instance is proved directly.
Every higher-rank instance reduces to strictly smaller certified dependencies.
The open work
What must happen next.
Version 4.1 is a systems and certificate proposal with exact lifting and induction theorems, not yet a proof-assistant implementation and not a shortcut around computational hardness. The exact kernel is Python/C++ rather than Lean, Isabelle, or Coq. The SAT distribution is synthetic. The dynamic program scales because its constraint has local structure.
The important next tests are whether proof-producing model counters can carry the interface to realistic formulas; whether theorem-proving agents can optimize certified rather than sampled witness mass; and whether the calculus can be formalized end-to-end in a proof assistant.
Explanation here. Evidence in the journal.
The journal identifier, immutable PDF, source, reproducibility files, review ledger, and GitHub release will appear only after the remaining publication gates pass.