Herein a Quantum Gödel Machine is defined as a self-rewriting, proof-driven agent whose acceptance gate for self-modifications is allowed to depend on quantum witnesses and quantum program logic, rather than only on classical proof strings. The central move is to promote quantum proofs to first class internal objects, a candidate rewrite is executed only when there exists a quantum witness state that makes a quantum verifier accept a formal claim that the rewrite increases a specified quantum utility functional while preserving formally stated safety constraints. The paper introduces an operator-level decomposition of self-rewrite dynamics in which proof search, verifier checking, and environment interaction jointly induce a completely positive map on the agent’s internal state and policy representation. Within this representation, stability of iterative self-rewrites is controlled by a spectral radius condition on a linearized update operator, and achievable improvement rate is bounded by information throughput across the agent-environment channel. The resulting framework yields two kinds of technically sharp statements, conditional complexity leverage claims that separate quantum-witness verifiability from classical-certificate verifiability for natural classes of self-improvement obligations, and measurable rate constraints that tie certified self-improvement to channel capacities and verification costs. The definitions isolate what is genuinely quantum in the construction and provide a path to both theorem-driven and system-level empirical evaluation.
Herein a Quantum Gödel Machine is defined as a self-rewriting, proof-driven agent whose acceptance gate for self-modifications is allowed to depend on quantum witnesses and quantum program logic, rather than only on classical proof strings. The central move is to promote quantum proofs to first class internal objects, a candidate rewrite is executed only when there exists a quantum witness state that makes a quantum verifier accept a formal claim that the rewrite increases a specified quantum utility functional while preserving formally stated safety constraints. The paper introduces an operator-level decomposition of self-rewrite dynamics in which proof search, verifier checking, and environment interaction jointly induce a completely positive map on the agent’s internal state and policy representation. Within this representation, stability of iterative self-rewrites is controlled by a spectral radius condition on a linearized update operator, and achievable improvement rate is bounded by information throughput across the agent-environment channel. The resulting framework yields two kinds of technically sharp statements, conditional complexity leverage claims that separate quantum-witness verifiability from classical-certificate verifiability for natural classes of self-improvement obligations, and measurable rate constraints that tie certified self-improvement to channel capacities and verification costs. The definitions isolate what is genuinely quantum in the construction and provide a path to both theorem-driven and system-level empirical evaluation.
We present the Infinity Machine, a self-improving AI agent that we use for research on problems whose answers aprogram or data can check. Each candidate solution is produced by a full tool-using agent that works for up to an hour in a fresh sandbox; proposers see only a public score, and a private split decides what counts. The harness itself(prompts, tools, skills, playbook, meta agent) is an editable genome, changed only through a kernel-enforced gate with held-out and cost checks. An autonomous mode goes from a plain-text goal to a verified report with no human step: an agent picks an open problem and writes its verifier, the kernel calibrates it, an adversarial agent audits it, and an agent that never sees the verifier re-checks the result. Across fourteen problems in six days, for about $180 of model usage, the system produced four results beyond the published state of the art on catalogued open problems in quantum information: a certified depolarizing-channel threshold point p = 0.064966, a qutrit positivity frontier of 0.2910672, a 44-gate depth-6 Golay state preparation, and a stabilizer-rank bound chi(T^7) <= 10. It also cut SABRE qubit-routing overhead from 68,559 to 12,087 added gates. In hardware, it cut the energy per MAC of an open 8x8 INT8 systolic tile by 77.7% through a full open RTL-to-GDS flow, bit-exact. Three fully autonomous runs ended in honestties with public records; one audit caught a stale record, and one agent-written score pointing the wrong way went unnoticed. We report the failures as carefully: the one self-derived harness generation was rejected on cost, proposers gamed lenient scorers four times, and operator changes were decisive for several results.
Process matrices describe correlations with no definite order of operations, and the property that sets a genuinely indefinite process apart from an ordinary mixture of ordered ones is called causal nonseparability. This paper gives a careful, self-contained account of why the whole framework hangs together consistently, across three levels at once, the level of plain probabilities, the level of quantum measurement rules, and the level of classical logical consistency. Its main practical result is an exact, written-out certificate that detects the indefiniteness of the canonical process by hand, replacing a numerical computer search with a formula a reader can check with pencil and paper. Working in a convenient basis in which the relevant bookkeeping operations act especially simply, the paper derives the certificate in closed form as the identity minus two specific order-sensitive terms. It shows that the two natural pieces of this certificate are well-behaved in the technical sense required, each with an explicit, exactly known set of values and an explicit proof of positivity written as a sum of squares. Evaluated on the canonical indefinite process, the certificate returns a specific negative number exactly, which is precisely the signal of indefiniteness. The paper then abstracts the construction into a general recipe, a theorem stating that any certificate of this shape is valid whenever a simple sum-of-squares condition holds on its two pieces. Alongside this it lays out, level by level, how the framework stays consistent, from the requirement that probabilities behave, through the quantum measurement rule, to the classical fixed-point picture in which a would-be paradoxical loop has, or fails to have, a unique consistent resolution. Every numbered result is also formally verified in a machine proof assistant, to the authors' knowledge the first such verification for this framework, with the correspondence to the formal statements collected in an appendix. The value of the paper is to turn what had been the output of an opaque numerical optimizer into a transparent, reusable, and independently machine-checked object that anyone can audit and build on. By exhibiting an exact certificate and a general recipe for producing more, it lowers the barrier to certifying indefinite causal order, and by verifying the whole consistency core in a proof assistant it supplies a dependable formal foundation for later work. The paper is modest about what it adds, presenting the physics of the canonical process as already known and offering instead an exact and verifiable rendering of it.
AI agents are increasingly capable of constructing quantum algorithms and proofs, yet machine-checked proofs alone cannot guarantee that the intended problem is solved or that resource claims match the verified computation. Here we introduce Lean-QuantumAlg, a Lean 4 framework for trustworthy AI-assisted development of quantum algorithms. Its Algorithm-Solves-Problem contract binds correctness, success probability, borrowed-state restoration and quantum and classical resource bounds to a single execution, while separating the guarantees that Lean checks from the problem specifications and execution models that humans review. We demonstrate the framework on nine AI-formalized quantum algorithms, from Grover search to quantum attacks on RSA-2048 and P-256, with less than 1% of each algorithm's imported source code requiring statement-level human review once the shared framework has been audited. By integrating reusable mathematical foundations, certified algorithmic primitives and execution-grounded verification, Lean-QuantumAlg provides a basis for AI agents to construct and certify quantum algorithms, opening a path toward scalable AI-driven discovery of quantum algorithms.
The Witnessed Difference Programme: From Finite Distinction to Witnessed Measurement develops a finite obstruction calculus that makes the assumptions behind mathematical and operational constructions explicit. Starting from an exhibited distinction, it examines what additional structure is required for retained witnesses, succession, duration, finite probability, observers, measurement, and weighted histories. The mathematical core includes finite symmetry obstructions, cochain complexes, quotient defects, closure diagnostics, and exact optimization certificates. Matching repair and dual witnesses certify an optimum under declared hypotheses. Presentation and adapter theorems characterize when compressed reports preserve specified operations, relations, and queries; counterexamples identify information that compression loses. These results provide concrete criteria for checking whether a proposed representation preserves its intended meaning. A layered observer architecture distinguishes presentation, memory, evaluation, and policy. Observation requires a registered, witnessed, re-accessible interaction accepted by a declared evaluator. Measurement adds a specified measurand, reported-value map, calibration, uncertainty, provenance, and any claimed metrological traceability. Permission and authority require their own declared rules. Version 0.5.0 consolidates the primitive-axiomatics and Genesis-alpha sources and develops additional bridges to the actual Genesis raising and marked-result constructions. Complete quotient keys retain directed assertions, loops, and joint incidence, while ordered raw histories preserve the information needed to replay declared costs and transitions. Nineteen historical targets receive finite or conditional resolutions through constructions, exact criteria, or counterexamples; the wider Genesis reconstruction obligations remain separately registered. A further extension connects Meron orbit cancellation to finite character sums and gives precise conditions for preserving observable numerators. The CODA-CS/Q branch develops conditional interval enclosures and refinement interfaces. Exact finite transfer traces and rational extrapolation illustrate the distinction between arithmetic error and model error: an enclosure for a finite interpolation calculation bounds a thermodynamic limit only when justified scaling-remainder bounds are supplied. The accompanying evidence architecture connects statements to implementations, tests, selected Lean 4 formalizations, source provenance, and independently checked receipts. Formal proofs, computational demonstrations, and physical interpretations retain their separate scopes. The contribution is an explicit framework for locating the assumptions, preservation conditions, and missing interfaces in a derivation. Quantum-capable representations are developed under declared inputs; unrestricted quantum reconstruction, Born-rule uniqueness, continuum physics, and the proposed higher-dimensional field-theory targets remain open.
The mathematical representation of the universe consists of sequences of symbols, rules and operators containing Gödel's undecidable propositions: information and its manipulation, also with Turing Machines. Classical information theory and mathematics, ideally independent from the medium used, can be interpreted realistically and objectively from their correspondence with quantum information, which is physical. Each representation of the universe and its evolution are, in any case, physical subsets of the universe, structured sets of observers and their complements in the universe made with spacetime events generated by local quantum measurements. Their description becomes a semantically closed structure without a global object-environment loss of decoherence as a von Neumann's universal constructor with a semantical abstract whose structure cannot be decided deterministically a priori from an internal observer. In a semantically closed structure, the realization of a specific event that writes the semantical abstract of the constructor is a problem of finding "which way" for the evolution of the universe as a choice of the constructor's state in a metastructure, like the many-world Everett scenario, from a specific result of any quantum measurement, corresponding to a Gödel undecidable proposition for an internal observer.
Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.