CollatzX
Computes Collatz trajectories, stopping-time features, parity ratios, and near-miss rankings for bounded runs.
Inspect CollatzXDirected search for mathematical counterexamples.
ProofX is an open Python research toolkit for ranking candidates, running bounded experiments, and publishing replayable ledgers. It is a search system, not a proof system.
Scope
A ProofX run evaluates a finite set of candidates under a fixed command, budget, seed, and code revision. If no counterexample is found, the result is reported as unrefuted at that budget.
- It can rank candidates, compute features, and write an audit ledger.
- It can help compare search strategies and reproduce bounded runs.
- It cannot prove Collatz, Goldbach, the Riemann Hypothesis, or any open conjecture.
Research Workflow
The useful artifact is the ledger: every evaluated candidate, feature vector, near-miss score, strategy label, and seed.
- Run a directed search with a pinned command and seed.
- Save the JSONL ledger, not only the top-k summary.
- Inspect high-ranking candidates and failed assumptions manually.
- Publish the command and limits next to any result table.
Engines
GoldbachX
Counts prime-pair partitions and ranks sparse even-number families by Hardy-Littlewood deficit.
Inspect GoldbachXRiemannX
Runs numerical diagnostics around zeta zeros, prime-counting approximations, and Keiper-Li coefficients.
Inspect RiemannXResults
Result pages should be read as run summaries. A table can show what a specific configuration found; it does not certify a conjecture.
- Near-miss scores rank candidates inside a strategy.
- Browser demos are small inspectors, capped for responsiveness.
- Unsupported benchmark claims are intentionally avoided.
FAQ
Does ProofX prove conjectures?
No. ProofX runs bounded searches and records the results. A negative run means no counterexample was found under that configuration.
What should I trust?
Trust the command, code revision, dependency environment, and ledger more than any summary sentence. Summaries are only views over run data.
Where does Lean 4 fit?
The root ProofX repository now includes a small Lean 4 package for bounded certificates. Germinal remains a separate vendored Lean 4 project.
Founder
Mohammed Alkindi
Building ProofX as a small, open research codebase for reproducible mathematical experiments and careful public reporting.
- Maintains directed-search engines for Collatz and Goldbach experiments.
- Focuses on ledgers, replay, and explicit limitations.
- Welcomes review from researchers and engineers interested in computational number theory.