Proposal to Harmonic's Aristotle Principal Investigator Sponsorship
Lakatos Square asks a basic question about frontier mathematical AI: can a community of autonomous agents make more reliable discoveries when some agents build proofs and others actively try to refute them?
The project will run replicated, preregistered 2×2 experiments in which autonomous mathematical agents pursue the Collatz problem for two months. Every condition contains a main researcher and an auxiliary researcher, works from the same bare Mathlib seed, and has the same ultimate standard: an exact result checked by Lean's kernel. The proposed next phase will run on Harmonic's Aristotle, whose Lean-native design and emphasis on formally verified mathematics make it an unusually strong match for the experiment.
The name comes from Imre Lakatos's Proofs and Refutations, where mathematics advances through a dialectic: conjectures generate proofs, proofs expose hidden lemmas, and counterexamples force better definitions and stronger arguments. “Square” refers both to the four cells of the experiment and to the attempt to turn that dialectic into a reproducible research design.
Simon DeDeo is a professor at Carnegie Mellon University, an External Professor at the Santa Fe Institute, and project leader of Proofs & Reasons, a Templeton-supported program on mathematical understanding, metamathematics, and AI-assisted proof discovery. His recent contributions include work on the relationship between informal and formal proof, empirical metamathematics and Lean theorem discovery, and the public collatz-program experiment that motivated this proposal.
The first axis changes the mathematical objective of the main agent:
- Prove: advance a substantial theorem near the full Collatz conjecture, centered on the Krasikov–Lagarias difference-inequality program and the endpoint question conventionally summarized as
lambda → 2. - Refute: construct a genuine Collatz counterexample—a nontrivial positive cycle or one positive integer with a formally certified nonterminating orbit—beginning from Alex Kontorovich's “hardware/software” and self-reproducing-program perspective.
The second axis changes the auxiliary agent's role:
- Sympathetic: monitor the main agent and build Lean definitions, lemmas, certificate consumers, and repairs that remove its most important bottlenecks.
- Adversarial: independently attack the main agent's strongest unproved assumption, formalizing counterexamples and no-go theorems even when the main requests help on a different line.
| Sympathetic auxiliary | Adversarial auxiliary | |
|---|---|---|
| Counterexample search | Construct formal bridges toward a concrete exceptional orbit | Try to prove that the current counterexample architecture cannot work |
| KL theorem | Construct formal bridges toward the lambda → 2 endpoint |
Try to falsify the current endpoint mechanism or its hidden lemmas |
Each cell contains exactly two agents, main and auxiliary. Thus one complete 2×2 replication contains eight autonomous agents. The conditions begin with byte-identical target corpora and main instructions; only the auxiliary-role treatment differs. The protocol uses immutable provenance, isolated repositories, regular progress snapshots, hourly human-readable diary entries, and a strategy review first at 4 hours 30 minutes and every four hours thereafter. Claims are not counted as mathematical results unless they have a kernel-checked Lean proof, an exact replayable certificate, or an explicitly bounded exhaustive verification.
Replication is central. A single dramatic agent trajectory is an anecdote; multiple independently seeded 2×2s can show whether proof-oriented and refutation-oriented processes differ systematically and whether adversarial collaboration is reliably useful.
- Counterexample / sympathetic — private, access available on request
- Counterexample / adversarial — private, access available on request
- KL / sympathetic — private, access available on request
- KL / adversarial — private, access available on request
The longer-running precursor is public at collatz-program. It contains the original Lean development, computational certificates, failure ledgers, and research diary from which the controlled experiment was designed.
The Collatz conjecture is elementary to state and exceptionally resistant to proof. It is therefore a stringent test of whether a mathematical agent can do more than retrieve a familiar technique, extend a routine formalization, or produce persuasive prose.
It also naturally supports the experiment's two directions.
On the proof side, the Krasikov–Lagarias difference inequalities give a concrete, finite-level route to nontrivial lower bounds on the number of integers known to reach 1. The project studies whether a sequence of finite optimization parameters approaches the endpoint 2. Proving that endpoint would yield a major strengthening of known predecessor-counting results, though it would not by itself prove the full Collatz conjecture.
On the counterexample side, the dynamics can be treated as fixed hardware and the initial integer as software. Finite valuation words can be synthesized exactly, suggesting programs built from separated binary packets, timed carry collisions, modular controllers, or self-reproducing “gliders.” The difficulty is not making an arbitrarily long finite trajectory; it is stabilizing all of those finite instructions into one ordinary positive integer with an exact nontermination certificate.
This combination is rare: one problem admits a deep theorem-building program, a concrete counterexample-engineering program, inexpensive exact computation, and a natural formal language in Lean.
“Prove the conjecture” and “find a counterexample” are not simply opposite answers to the same search query. They reward different representations, intermediate lemmas, uses of computation, and standards of evidence.
A proof-oriented system may seek monotonicity, compactness, induction, or a transfer theorem. A counterexample-oriented system may seek a finite-state certificate, an exceptional congruence class, or a self-reproducing orbit. Running both directions under a shared protocol lets us ask whether frontier models have a directional bias: are they better at extending universal arguments, constructing exceptional objects, or discovering why a proposed route is structurally impossible?
Whichever side fails can still produce mathematics. A failed counterexample architecture can yield a universal no-go theorem; a broken proof can expose a false lemma and motivate a corrected theorem. Lean makes these negative results durable rather than anecdotal.
Lakatos argued that mathematics grows through the improvement of conjectures under criticism, not through a monotone accumulation of polished final proofs. Counterexamples can be global, refuting a conjecture, or local, refuting a hidden lemma while preserving a repaired route.
Current AI research workflows usually optimize for a helpful assistant. Lakatos Square directly tests a different institution: an auxiliary agent rewarded for finding the cheapest exact obstruction to the main agent's present strategy. The sympathetic and adversarial conditions distinguish two possibilities:
- progress comes mainly from adding more proof labor to the main line; or
- progress comes from organized dissent that kills seductive but unproductive approaches early.
This matters beyond Collatz. If adversarial formal collaboration improves discovery, it suggests a scalable architecture for mathematical research groups of AI agents: conjecturers, proof builders, counterexample hunters, and formal auditors interacting through machine-checkable artifacts.
The precursor and pilot runs have not proved Collatz or produced a counterexample. They have nevertheless produced several concrete signals that justify a larger Aristotle experiment.
The public precursor reconstructed a substantial Krasikov–Lagarias development. It includes a fully Lean-native finite certificate at level k = 12, supporting a predecessor-counting exponent of approximately 0.8531, and a larger mixed exact-computation/kernel-checked result at k = 19, supporting every fixed exponent below approximately 0.9094372617. The endpoint lambda → 2 remains open.
Formal auditing also found concrete counterexamples to intermediate identities and induction principles used in the printed KL route, then built an occurrence-aware history and elimination framework that avoids those failures. This is precisely the kind of outcome the project values: refutation does not merely reject a proof; it reveals the object a corrected proof must track.
In the first twelve hours of the controlled 2×2:
- Counterexample / sympathetic constructed an exact parameterized ordinary-Collatz boundary macro, then imported an auxiliary modulo-eight theorem proving that its simplest direct closure is impossible. The surviving route requires a support-changing controller rather than a larger blind search.
- Counterexample / adversarial proved that every pure power-of-two finite carry trap is empty and pushed the surviving architecture into genuine interaction between multiple binary bits and an odd factor. This replaced finite scanning with a symbolic all-depth obstruction.
- KL / sympathetic developed history-labelled fiber events, positive delay gaps, high-water potentials, and a bound on all-
nexttails. Its remaining gap is a global infinite-branch/well-founded-tree argument connecting the local machinery to termination. - KL / adversarial proved exact level monotonicity and reduced the endpoint to cofinal admissibility below 2. Its auxiliary independently ruled out an every-level tight-prefix mechanism at level three, leaving eventual-prefix or parameter-improving mechanisms as the honest alternatives.
The adversarial auxiliaries are measurably behaving differently from the sympathetic auxiliaries. They have initiated attacks without main-agent requests, declined requested proof labor when a more fundamental assumption was vulnerable, and caused strategy pivots after producing checked obstructions. The sympathetic auxiliaries, by contrast, are more often producing importable bridge lemmas requested by the main.
These are preliminary, agent-side checked results. Final claims will undergo detached replay from clean environments before publication. At present there is no Collatz counterexample and no proof of the KL endpoint.
The proposed award supports sixty days of autonomous work using Aristotle Agent/API access, with frozen experimental conditions and independent replication. Aristotle is especially appropriate because it is designed to work directly in Lean projects and return formally verifiable artifacts rather than natural-language claims alone.
The primary outputs will be:
- new kernel-checked theorems, counterexamples to intermediate claims, or exact certificates relevant to Collatz and the KL endpoint;
- a replicated causal comparison of proof versus counterexample objectives and sympathetic versus adversarial collaboration;
- a public taxonomy of successful and failed mathematical-agent strategies;
- reproducible prompts, frozen seeds, Lean source, certificate manifests, review records, and a final comparative report; and
- design guidance for future communities of formally verified mathematical agents.
Success is deliberately plural. A proof of the endpoint or a genuine Collatz counterexample would be extraordinary. A family of new no-go theorems, a repaired KL argument, or robust evidence that adversarial auxiliaries improve theorem discovery would also advance mathematics and the science of mathematical reasoning.
Harmonic's sponsorship combines direct support for ambitious PI-led projects with access to next-generation Aristotle models. Because Aristotle currently publishes no usage fee, the budgets below separate cash support from the requested Aristotle workload capacity rather than assigning an invented dollar price to model access.
One current 2×2 replication—eight agents—processed 1.892 billion gross tokens in twelve hours. This comprised 1.885 billion input tokens, of which 1.849 billion were cached input, and 6.70 million output tokens. Holding that observed cadence fixed for sixty days gives:
| Replications | Concurrent agents | 60-day gross-token proxy | Cached input | Uncached input | Output |
|---|---|---|---|---|---|
| 1 | 8 | 227.1 billion | 221.9 billion | 4.32 billion | 0.804 billion |
| 4 | 32 | 908.2 billion | 887.7 billion | 17.28 billion | 3.216 billion |
| 8 | 64 | 1.816 trillion | 1.775 trillion | 34.55 billion | 6.432 billion |
These are capacity-planning figures measured from Codex session telemetry, not a claim about Aristotle's tokenizer, cache policy, billing units, or eventual consumption. The award request is for enough Aristotle access to sustain the corresponding research duty cycle; Harmonic can translate the workload into its internal serving units.
The reference host, akdeniz, has an AMD Ryzen 9 7950X with 16 physical cores/32 threads, 128 GiB RAM, and approximately 11 TB of local experiment storage. The planning allowance is $4,000 per comparable host, including memory, storage, enclosure, cooling, power supply, and integration. This is a budget allowance rather than a vendor quotation.
| Level | Experimental scale | Local infrastructure | Faculty support | Direct cash request | Aristotle access request |
|---|---|---|---|---|---|
| Top — Full Lakatos Square | 8 complete 2×2 replications; 64 agents for 60 days | 4 comparable hosts: $16,000 | 3 months at $183,000/year: $45,750 salary + $11,712 fringe | $73,462 | Capacity for approximately 1.816 trillion gross tokens |
| Mid — Replicated Square | 4 complete 2×2 replications; 32 agents for 60 days | 2 comparable hosts: $8,000 | — | $8,000 | Capacity for approximately 908.2 billion gross tokens |
| Base — Continuity | Continue 1 complete 2×2; 8 agents for 60 days | Existing host | — | $0 | Capacity for approximately 227.1 billion gross tokens |
The top-tier fringe estimate uses Carnegie Mellon's latest published FY2026 domestic full-time rate of 25.6%. The salary line covers preparation, two months of live supervision and scientific interpretation, detached proof verification, analysis, and public reporting. Institutional facilities and administrative costs, if required, are not included and would be resolved with Carnegie Mellon's sponsored-programs office. Hardware totals also exclude any sponsor-specific indirect costs.
- Every experimental condition starts from a documented bare seed and immutable prompt manifest.
- Main and auxiliary work is isolated by condition; no cell can inspect another cell's results during the run.
- Numerical evidence is labeled as evidence. Lean theorems, replayable certificates, and bounded exhaustive checks are reported separately.
- Negative results and failed strategies are preserved rather than silently discarded.
- Final mathematical claims are replayed from clean environments and checked for
sorry, new axioms, unsafe shortcuts, and definition drift. - Aggregate protocols and results will be released publicly. The four live research repositories remain private during the experiment to preserve isolation and credential safety; access is available on request, followed by a reviewed public release where appropriate.
Lakatos Square is both a serious attack on difficult mathematics and an experiment in how mathematical communities of machines should be organized. Harmonic's combination of frontier mathematical reasoning, Lean verification, and support for public research makes Aristotle the natural platform for the next phase.