ProofX

ProofX is a research toolkit for directed counterexample search in discrete and analytic number theory. It currently focuses on Collatz, Goldbach, and Riemann Hypothesis-adjacent numerical experiments. The project is deliberately framed as search and evidence tooling, not as a proof system.

The central rule is simple: when a run finds no counterexample, the result is reported as unrefuted at this budget. That does not mean true, verified, validated, likely, or proved. It only means that the configured search did not find a disproof.

Current Scope

ProofX contains three kinds of material:

Area	Status	Role
packages/python/codebase/	Active Python research toolkit	Runs directed searches, computes features, writes ledgers, and exposes the CLI.
ProofX/	Root Lean 4 certificate layer	Checks small bounded artifacts and status semantics.
docs/	Maintainer and research documentation	Describes assumptions, algorithms, run semantics, and limitations.
src/	Static research site	Presents the project, demos, and result summaries without changing the engine behavior.
packages/germinal/	Vendored sibling project	Separate Lean 4 conjecture-generation and proof-attempt system, synced by subtree.

packages/germinal/ has its own README and operating rules. Keep ProofX-root changes separate from Germinal changes unless a task explicitly crosses that boundary.

What ProofX Does Not Claim

ProofX does not prove Collatz, Goldbach, the Riemann Hypothesis, or any related open conjecture.

ProofX does not certify mathematical truth from empirical runs.

ProofX does not treat high near-miss scores as probabilities of falsehood. A score ranks candidates inside this toolkit's search strategy; it is not a calibrated belief.

ProofX does not make benchmark claims unless a run ledger, command, hardware context, and version information are provided.

Directed Search

Uniform scans are useful for bounded verification, but they are not what this repository is mainly testing. ProofX asks a narrower question: if a counterexample existed, what structural signals might make a candidate worth checking first?

Current strategies:

Engine	Search idea	Output
Collatz	Expand from known high stopping-time anchors and score trajectories by growth, parity, entropy, and excursion features.	Candidate ledger with convergence diagnostics and near-miss scores.
Goldbach	Search structurally sparse even numbers whose observed partition count is low relative to Hardy-Littlewood prediction.	Candidate ledger with partition counts, deficits, and residue-family metadata.
Riemann	Compute numerical signals from zeta zeros and Keiper-Li coefficients.	Numerical diagnostics only; not a proof of RH or a certified zero computation.

The shared FalsificationEngine writes every evaluated candidate to JSONL. The ledger is the audit trail: it records candidate, conjecture label, strategy, feature vector, score, details, timestamp, and RNG seed.

Architecture

ProofX/
  packages/python/codebase/
    FalsificationEngine/     Directed search orchestration and ledgers
    CollatzX/                Collatz sequence features and related experiments
    GoldbachX/               Prime sieve, partitions, and structural filters
    ReimannX/                Riemann-related numerical experiments
    CrossEngineAnalysis/     Correlation tooling for ledgers
    cli.py                   Unified CLI
  ProofX/                    Root Lean 4 certificate definitions
  ProofX.lean                Root Lean import file
  lakefile.lean              Root Lake package
  lake-manifest.json         Lake package manifest
  lean-toolchain             Pinned Lean toolchain
  tests/                     Root pytest suite for ProofX codebase
  docs/                      Project documentation
  src/                       Static site: source subdirs + deploy output; served by Vercel
  packages/germinal/         Separate vendored Lean 4 project

See docs/architecture.md for the fuller maintainer map.

Local caches, virtual environments, generated run outputs, and old root-level scratch folders are intentionally ignored. On Windows, run scripts/cleanup.ps1 -Deep; on Unix shells, run ./scripts/cleanup.sh --deep. Do not move the old Germinal tree back to the root: it belongs under packages/germinal/.

Lean 4 Boundary

The root Lean package checks bounded certificates produced by the search, not hand-written samples. python -m codebase.cli export lean reads the ledger and writes one named theorem per certifiable row into ProofX/Generated/LedgerCertificates.lean:

theorem collatz_27_reaches_one :
    reachesOneWithin 111 27 = true := by
  decide

theorem goldbach_28_has_pair :
    goldbachPair 28 5 23 3 5 = true := by
  decide

The first says 27 reaches 1 within 111 steps. The second says 28 is even and at least 4, that 5 + 23 = 28, and that both summands are prime — each verified against a trial-division bound the exporter supplies, so the kernel checks one multiplication instead of computing a square root. isPrime_of_isPrimeWithBound proves once that such a bound really does establish primality.

These are finite checks, not evidence. 500 certificates are 500 bounded facts. None states or implies Collatz or Goldbach, and a passing build says nothing about either conjecture.

Every proof closes with decide, so the Lean kernel checks it. native_decide is barred: it evaluates via compiled native code and trusts the result through Lean.ofReduceBool and Lean.trustCompiler, which would widen the trusted base to the compiler and runtime. ProofX/Audit.lean enforces this during lake build by walking each theorem's real axiom dependencies — a textual scan cannot see an axiom introduced by a tactic.

lake build                                  # kernel-check + axiom audit
python -m codebase.cli export lean          # regenerate from the ledger
python -m codebase.cli export lean --check  # fail if they drifted

See docs/lean4.md for the formal boundary and acceptance bar.

Near-Miss Scoring

Both falsifiers reduce a candidate to a ranking score in [0, 1].

Collatz:  near_miss = 0.70 * risk_score + 0.30 * excursion_bonus
Goldbach: near_miss = 0.85 * deficit    + 0.15 * structural_hardness

These are ranking functions, not proof certificates. They decide what the search inspects first and what the report surfaces. If a weight changes, the corresponding derivation in docs/engines/falsification.md must change with it.

Reproducibility

Engine randomness flows through a seeded NumPy generator. Child seeds are derived deterministically so that a target-specific run can be compared with a combined run at the same master seed.

rng_master = np.random.default_rng(seed)
collatz_seed, goldbach_seed = rng_master.integers(0, 2**31, size=2)

Every evaluated candidate can be written to JSONL:

{
  "candidate": 12345,
  "conjecture": "collatz",
  "strategy": "inverse_tree_beam_search",
  "features": {
    "lyapunov_exponent": 0.0412,
    "hurst_exponent": 0.5831,
    "parity_ratio": 0.5714
  },
  "near_miss_score": 0.2847,
  "rng_seed": 1234567890
}

Reproducibility depends on the Python version, dependency versions, platform math libraries, and code revision. Keep the command, seed, dependency lockfile, and ledger together when publishing results.

Quickstart

git clone https://github.com/MohammedAlkindi/ProofX.git
cd ProofX

python -m venv .venv
source .venv/bin/activate          # Windows: .venv\Scripts\activate
pip install -r requirements.txt -e .

python -m codebase.cli falsify --budget 200 --seed 42 --target both

Research Workflow

# 1. Run a directed search and save the full ledger.
python -m codebase.cli falsify \
    --budget 2000 --seed 42 --target both \
    --save-ledger results/ledger.jsonl \
    --output-json results/summary.json

# 2. Inspect the ledger in the static viewer.
open src/ledger-viewer.html

# 3. Hand-label entries, then fit a calibrator.
python -m codebase.cli calibrate fit \
    --ledger results/ledger_labelled.jsonl \
    --method isotonic \
    --output results/calibrator.pkl

# 4. Annotate a ledger with calibrated scores.
python -m codebase.cli calibrate annotate \
    --ledger results/ledger.jsonl \
    --calibrator results/calibrator.pkl

# 5. Compare near-miss neighborhoods across engines.
python -m codebase.cli correlate \
    --collatz results/collatz.jsonl \
    --goldbach results/goldbach.jsonl \
    --radius 200

# 6. Export certifiable rows as Lean theorems and kernel-check them.
python -m codebase.cli export lean --ledger results/ledger.jsonl
lake build

Testing

The repository policy expects these checks before a commit:

pytest
ruff check .
ruff format --check .
mypy packages/python/codebase
lake build
npm install
./scripts/build.sh
./scripts/validate-links.sh

The badges describe the intended quality floor, not a mathematical guarantee. If a check is failing, note that explicitly in any published result or release.

Documentation

Doc	Covers
docs/architecture.md	Project boundaries, data flow, ledgers, and status semantics.
docs/research-standards.md	Language standards for claims, evidence, and public copy.
docs/lean4.md	Root Lean package scope, certificate rules, and acceptance bar.
docs/engines/falsification.md	Shared scoring, ledger schema, and directed-search assumptions.
docs/engines/collatz.md	CollatzX model, features, and limits.
docs/engines/goldbach.md	GoldbachX sieve, partition, and deficit logic.
docs/deployment.md	Static site deployment and validation notes.
docs/content-strategy.md	Tone and site-copy guidance.
docs/mvp.md	Minimum viable tooling bar (CI, packaging, local checks) and current gap status.
docs/ROADMAP.md	Open workstreams and non-goals, at a glance.

License

MIT. See LICENSE.