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 retained v3 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 6 · A practical guarantee
Three promises, each with its own evidence.
Think of a calculator that hands you a receipt you can check. The receipt establishes that this answer is correct. To promise an answer for every allowed input, you need another record: a complete inventory of that domain with a checked result for every member. To describe how often it succeeds on future inputs, you need a sampling plan and a reliability calculation.
- Exact answer
A witness you can inspect.
The wrapper releases an answer only after the exact checker accepts it. A failed search remains unresolved.
- Complete finite domain
12,673 out of 12,673.
Every primitive open seven-speed set in the declared 1–20 domain has a verified witness. Another checker reconstructs the domain to confirm nothing was skipped.
- Fresh-input evaluation
4,603 trials. Zero failures.
A fixed test on uniform seven-speed subsets of 1–60 supports at least 99.9% verified-answer availability at 99% confidence, under its stated IID assumptions and frozen solver.
The percentage concerns how often the system returns a checked answer. It does not turn mathematical truth into a confidence score. These inputs were generated for a mathematical laboratory test; physical-world claims would need actual measurements and a deployment protocol.
A useful failure helped shape the implementation. The proposed short list of canonical targets missed (44, 60, 104, 205), even though 9/148 is a valid witness time. The solver now retains a complete fallback instead of treating a favorite search pattern as a universal theorem.
Read the precise contracts · Download the code and full evidence.
Version 5 consolidates corrected arithmetic results, probability calculations, and a reusable certificate checker. It is not a proof-assistant formalization or a universal solution. 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.
Updated September 5 · Version 5
Better proof tools. A precisely stated remaining gap.
Imagine a search that can take wrong turns, but must return a receipt whenever it finds a solution. The follow-up SWC checker can verify those receipts, combine their exact probabilities, and check formulas for every member of an infinite family. The latest kernel passes 24 tests and combines twelve infinite families without treating their union as all primes.
Filtering out candidates with the wrong arithmetic character improves the specified recursive sampler by 1.5×–2.5× when its original success mass is positive. A separate comparison of ten samplers on eight difficult primes found useful gains, but no overall winner. These improve search and verification; they do not prove that every prime has a successful candidate.
The final literature pass found exact parametrizations, sparse exceptional sets, and conditional probability tools, but no theorem that closes the missing pointwise existence claim. Read the evidence and corrected proofs or download the lightweight research supplement.
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 preprint PDF and follow-up supplement are available now. An accepted journal identifier, reviewed immutable deposit, and formal release remain subject to the publication gates.