An AI research notebook beyond the known proof barriers.
PvsNP-Cartography is a long-horizon research notebook for exploring the P vs NP problem with AI-assisted mathematical research.
The objective is deliberately not:
“Generate a proof of P ≠ NP.”
The objective is:
Map what is known, identify what known proof barriers actually rule out, explore the remaining terrain, attack every new claim adversarially, and preserve both discoveries and failures as durable research artifacts.
A solved Millennium Prize Problem would be extraordinary.
A careful map of why our attempted routes fail is still useful.
This repository is governed by five rules.
-
Known results come first.
Before proposing a route, identify the theorems, lower bounds, and proof barriers that already constrain it. -
Every claim gets attacked.
A proposed lemma is not progress until we have actively tried to falsify it, found edge cases, checked definitions, and searched for known counterexamples or prior art. -
Finite evidence is not an asymptotic proof.
Computation can suggest structure and kill conjectures. It cannot silently become a theorem about all input sizes. -
Formalization is verification, not decoration.
Lean/Coq or another proof assistant should be used where feasible for surviving lemmas and known-result reconstruction. -
Failure is data.
Dead approaches go to the graveyard with a clear explanation of why they died, so the same seductive error is not rediscovered every week.
P vs NP has enormous prior literature and several famous proof barriers.
A useful AI research process therefore resembles exploration more than proclamation:
- chart known territory
- mark impassable walls
- identify poorly explored boundaries
- conduct small expeditions
- bring back only claims that survive hostile review
The repository is intended to preserve that map over time.
The first map should include at least:
- P, NP, NP-completeness, Cook–Levin
- circuit complexity and lower bounds
- proof complexity
- communication complexity
- SAT and restricted models
- relativization
- Natural Proofs
- algebrization
- known lower bounds for restricted circuit classes
- algorithmic lower-bound connections such as the Williams program
- formalization opportunities in Lean
The project should prefer small, sharply stated subproblems over vague attacks on the whole conjecture.
Planned structure:
map/ known terrain, definitions, barriers, open directions
prior-art/ audits of external projects and systems
expeditions/ bounded research attempts with explicit hypotheses
claims/ claims that currently survive internal attack
attacks/ adversarial reviews, counterexample searches, failure analysis
experiments/ finite computation and reproducible scripts
formal/ proof-assistant artifacts
graveyard/ dead approaches, false lemmas, seductive mistakes
logs/ chronological research sessions
A useful claim should carry an explicit state.
- idea: plausible direction, not checked
- candidate: precisely stated and under attack
- finite-evidence: supported only on bounded computation
- literature-consistent: checked against known references, not novel by default
- formally-verified: accepted by a proof assistant under explicit assumptions
- refuted: counterexample or invalid step found
- novelty-unknown: may be new, but prior-art search is incomplete
- novelty-supported: targeted prior-art search found no equivalent result; still not a publication claim
No file should casually jump from “interesting” to “proved.”
For each expedition:
- state the exact target
- record relevant known results/barriers
- propose one or more approaches
- derive the smallest testable lemma
- search for counterexamples
- run finite experiments where useful
- conduct an adversarial self-review
- compare with prior literature/projects
- formalize surviving statements with audited assumptions
- either promote the claim or bury it with a post-mortem
The default loop is:
hypothesize → attack → repair → attack again → verify → record
This project is not the first attempt to use AI around P vs NP.
Early comparison targets include:
- GISMO-1/p-vs-np-hunter: multi-agent circuit/lower-bound exploration with Lean-backed verification
- LLMDeveloperAiPNP/LLM-Developer-AiPNPvs-NP---Autonomous-Solver-Ai: autonomous multi-agent solver architecture
- MuchuCAT/p-vs-np-ai-quantum-research-notes: conservative dossier on proof barriers and AI/quantum narratives
- RenaudGL/Protocol_Cathedrale: multi-model exploration of a thermodynamic route to P ≠ NP
These projects are prior expeditions, not targets to imitate blindly.
Their successes, omissions, failure modes, and methodological choices should be mapped before duplicating work.
See prior-art/ as it develops.
Progress can be much smaller than solving P vs NP.
Examples:
- a clean machine-checkable reconstruction of a relevant known result
- a new finite pattern that survives replication and has a plausible asymptotic interpretation
- a conjecture with a precise falsification path
- a useful reduction between narrowly defined subproblems
- a rigorously documented dead end that eliminates a tempting family of approaches
- a genuinely new lemma that survives literature search and formal verification
- a better research protocol for AI-assisted open mathematics
- “The model feels confident.”
- A long proof-shaped text with an unchecked step.
- Numerical agreement for small n presented as asymptotic truth.
- Renaming a known theorem.
- Ignoring relativization / Natural Proofs / algebrization because they are inconvenient.
- A proof assistant file with unproved axioms hidden behind impressive names.
- A literature search that only asks an LLM from memory.
- Declaring novelty before searching.
P vs NP attracts false proofs for good reason: the gap between “this argument is compelling” and “this argument is valid” is enormous.
This repository therefore treats self-criticism as part of the research object.
The most valuable file in a research session may be the one explaining why the idea failed.
- AGENTS.md: research operating contract for AI collaborators
- docs/RESEARCH_PROTOCOL.md: adversarial research loop and publication threshold
- Research direction and conceptual dependency map: scientific target selection, contribution types and the next structural bridge
- docs/PRIOR_ART.md: direct P vs NP AI projects and broader AI-mathematics systems
- docs/BIBLIOGRAPHY.md: working primary-source bibliography
- map/BARRIERS.md: relativization, Natural Proofs, and algebrization map
- Expedition 001: audit of p-vs-np-hunter finite-degree findings
- Expedition 002: finite MOD3 probabilistic-degree certificates, reproducible checker, and CI
- Expedition 003: historical exact sample-restricted n=8 dual and adversarial counterexample. Its sampled optimum did not decide the full n=8 problem.
- Expedition 004: exact n=8 degree-two certificate, checker, finite argument, and successful CI.
- Expedition 005: concrete n=5 Lean lower/upper certificate components, exact scope, and independent data audit.
- Expedition 006: complete n=5 degree-based Lean equality, statement audit, verified conclusion, and quantifier countermodel.
- Expedition 007: complete n=6/n=7 Lean equalities, compact 18-polynomial certificates, exact audit, verified conclusion, and failed cyclic compression.
- Expedition 008: generic full symmetrization, MOD3 applications, verified scope, exact audit and seven invalid shortcuts.
- Expedition 009: verified Hamming-layer counting and the complete n=8 Lean degree equality, with completion evidence.
- Expedition 010: n=8 repair and compact-witness recovery, 159-row certificate, exact validators and failed probability rounding.
- Expedition 011: exact n=9 one-orbit GF(2) MOD3 degree equality, strict 85/126 seed certificate, reproducible validators, bounded 7432-pattern search, and formally verified conclusion.
- Expedition 012: scoped failure of the restricted n10 single-orbit search; not a universal quadratic lower bound.
- Expedition 013: exact n10 eight-orbit certificate and universal affine-row dual.
- Expedition 014: original n10 formal candidate, independent coefficient audit and historical interrupted execution; completed by Expedition016.
- Expedition 015: preserved n11 nine-orbit and three-orbit finite certificates, validators and original CI evidence.
- Expedition 016: completed n10 formal repair, statement audit, isolated diagnostics and preserved failures.
- Expedition 017: exact n11 496-row same-measure compression, verifier/generator, actual CI evidence and invalid-weighting counterexamples.
- Expedition 018: complete n11 degree equality, conclusion, actual axiom output and independent source-data audit.
- Expedition 019: verified pure real-algebra score bound, original scope and bounded computational checks; its generic counting connection is separately completed by Expedition020.
- Expedition 020: generic actual-degree-one obstruction for every n>=7, actual-cube measure and counts, verified conclusion, actual axiom report, independent exact audit and preserved overcounting/build failures.
- Expedition 021: explicit balanced input fibers, generic guarded Hamming intersections, verified conclusion, actual axiom report, exact replication and range/multiplicity counterexamples.
- Expedition 022: generic weighted layer profiles, actual clique-polynomial evaluator, formal evidence and the exact restricted n12 lift obstruction.
- Expedition 023: accepted real-mixture obstruction, matching restricted-game value9/14, actual execution evidence, statement audit and primary-source bridge.
- formal/ASSUMPTIONS.md: current formal scope, actual axiom reports and preserved historical ledgers.
- Finite dual scope: generic real-mixture lemma and its concrete n=5 affine application.
- Current status: the earliest unblocked task and exact evidence boundaries.
Research checkpoint: approved 2026-10-22 JST night, completed just after midnight on2026-10-23 JST. Issue #16 is complete; Issue #17 is the next substantive frontier. See CURRENT_STATUS and RESEARCH_DIRECTION. Future nightly work requires fresh approval; this checkpoint does not authorize another session.
Accepted code9410fa95 passed completed formal run39800322628: pinned Lean4.35.0-rc4/Mathlib9e6b3aac, whole-root --wfail, unchanged namespace axiom policy and all24 new target reports. Actual source, commit and full execution output were re-fetched. Evidence and the actual target transcript preserve the acceptance; this documentation commit is not a new formal execution.
The real-mixture interface now connects actual polynomial correctness profiles to the existing finite duality and full symmetrization. At n12, no finite normalized nonnegative REAL mixture of precisely zero/all q9/all r8 reaches pointwise success2/3. The dual bound is9/14. A matching finite primal attains 9/14, so the restricted game's value is exact. This primal sharpness is computational, not a separately compiled Lean minimax equality. A genuine q8 polynomial scores5/6 under the same dual; that support-boundary counterexample is also Lean accepted. The bound does not cover all quadratics.
Exact code772b0eac passed run39799669199. The checker evaluates all716 actual candidate polynomials on all4096 inputs, compares independent profiles, verifies the matching primal and attacks the support, quantifier and normalization shortcuts. Normal/-O outputs and stored results match. Failures and counterexamples survive in graveyard033..035.
Numerical exact degree-two coverage remains n5..11; generic degree-one exclusion remains n>=7. Unrestricted n12 degree remains unresolved here. No support/denominator minimality, mathematical novelty, arbitrary-n quadratic upper bound, new circuit lower bound, barrier escape or P-vs-NP result is claimed.
The source comparison reconstructs explicit independent-majority and residue-restriction adapters to a known growing-degree lower bound. Its hard source theorem is imported, not proved by this repository. #17 targets the first substantive low-degree agreement/dimension lemma behind that bound, not automatic n13 enumeration or an open-ended expansion of tooling.
Gemini's AI review #15 covers only old checkpoint0e30b5b7, not these new modules. Human review #8 is separate and nonblocking. New-code independent semantic review and a second kernel are not claimed. Novelty remains unknown.
Latest research session. The complete preceding README is archived byte-identically; older checkpoints and failure records remain in Git history and dated archives.
The research environment must continue telling the difference between:
- known
- conjectured
- experimentally suggested
- formally verified
- refuted
- genuinely unresolved
Research lead / AI investigator: 月野テンプレクス
Created with 山田佳江 as the human collaborator and repository steward.