Long-Horizon AI Agents: Engineering Lessons from a 30-Hour Autonomous Theorem Formalization Run

1. The Case: A Sample of a Long-Horizon Task

An extreme case has been cited repeatedly in the industry recently: a frontier reasoning model, running autonomously and without interruption, fully formalized a classic number theory theorem into a machine-checkable proof. It took about 30 hours in total.

Most onlookers have focused on the “AI proved a major theorem” angle. From an engineering perspective, however, the more interesting point is not the mathematical achievement, since the proof of that theorem has long been accepted by the mathematical community. It is the time scale of the task.

Traditional LLM applications work in units of “one request, one response,” with contexts measured in thousands of tokens. When they fail, a human can step in and take over. This case worked on a different kind of unit: a goal that requires tens of thousands of intermediate state transitions, spans many rounds of failed attempts and retries, and whose correctness is finally decided by an independent kernel.

Tasks like this are known as long-horizon tasks. They differ from ordinary conversational tasks in their engineering constraints:

Dimension	Regular reasoning tasks	Long-horizon autonomous tasks
Time span	Seconds	Hours to days
Intermediate state	Fits within a single context	Far exceeds one window and must be externalized
Correctness check	Subjective human judgment	Must be adjudicated automatically by a machine
Cost of failure	One retry	Large amounts of compute already spent
Key engineering skill	Prompt engineering	Orchestration, state management, sandboxing, observability

To turn 30 hours into a reusable methodology, we first need to answer one question: why has formal mathematical proof become a touchstone for this kind of capability?

2. Why Formal Proofs Are an Unforgiving but Ideal Test Bed

Formal proof tasks are unique because they combine three properties that are almost impossible to find together in any other domain.

First, there is a single, non-human arbiter. A model does not judge whether a proof is correct. Instead, the proof assistant’s trusted kernel returns a boolean verdict. This removes the most fragile part of LLM behavior, namely self-evaluation bias. Every reasoning step the model generates has to “pass security screening” by the kernel, and any step that looks plausible but is actually invalid is rejected immediately.

Second, the feedback signal is extremely dense. Every strategy attempt returns a structured failure reason: the goal was not closed, a type mismatch occurred, or an assumption was not discharged. These error messages are valuable inputs for the next round of search. Together they form a natural self-supervised learning signal.

Third, the task cannot be gamed. The model cannot get by on surface patterns from memory, because the kernel does not recognize how fluent a narrative sounds. It only checks formal validity. This makes formalization a clean measure of whether a model truly has multi-step compositional reasoning ability.

The trade-off is that the task is extremely sparse and expensive. Formalizing a complete theorem often requires hundreds of thousands of lines of proof scripts and may involve thousands of intermediate lemmas. An error in any single step can force downstream work to be redone in full. This is a major reason the task was hard to automate until now.

3. Decomposing the Capability: Where Long-Horizon Agents Excel

To extract the engineering value of cases like this, the “30 hours” needs to be broken down into sub-capabilities that can be optimized independently.

3.1 Goal Decomposition and Proof Blueprints

Successful long-horizon formalization is rarely achieved by moving forward in a straight line. In practice, the model first produces a proof blueprint. It decomposes the main proposition into several lemmas, defines the dependency relationships between them (a DAG), and then fills in the proof one node at a time.

The blueprint turns a single, unsearchably large state space into a set of subproblems that can be solved independently and verified in parallel.

The engineering lesson is that the first stage of any long-horizon task should not be “start working right away.” It should be “produce a plan structure that can be checked.” Every node in the plan needs a clear completion criterion.

3.2 Externalizing State and Compressing Context

A 30-hour run inevitably produces far more intermediate information than a context window can hold. The practical approach is to move state out of the “conversation history” and into addressable storage:

• Serializing proof state: encode the set of proof obligations still to be closed, the assumptions established so far, and the lemmas already cited into a compact snapshot that identifies each search node.
• Deduplication and memoization: hash states to avoid repeatedly spending compute on the same equivalent state.
• Layered summarization: for early failed attempts, keep only a conclusion-level summary (for example, “this path fails at lemma X for reason Y”) and archive the raw logs to a log service instead of putting them into the context.

The core idea is that the model only decides “what to do next,” while an external system maintains the actual state ledger.

3.3 The Proof Search Loop

A typical inner loop looks like this (illustrative pseudocode, not any specific implementation):

state   = initial_state(theorem)
queue   = priority_queue(key = heuristic_score)   # sort by heuristic distance to closing the goal
budget  = { wall_clock: 30h, max_attempts: 1e6, token_cap: N }
while not queue.empty() and budget.remaining():
    node = queue.pop()
    for tactic in model.propose(node, top_k=32):        # model proposes candidate tactics
        nxt = kernel.check(apply(tactic, node))         # trusted kernel adjudicates
        if nxt.rejected:
            failures.record(node, tactic, nxt.reason)   # failure reason goes into the experience store
            continue
        if nxt.goals.is_empty():
            return nxt                                # all proof obligations closed
        key = hash(nxt.canonical_form())
        if key in cache: continue                     # deduplicate states
        cache.put(key, nxt)
        queue.push(nxt, heuristic_score(nxt))
return VerificationFailed(budget.exhausted)

The design rests on three key principles:

• Separate candidate generation from verification: the model provides breadth, and the kernel guarantees correctness.
• Treat failures as data: failure reasons constrain later sampling, which works much like online pruning.
• Set a hard budget ceiling: this prevents search divergence from causing costs to spiral out of control.

3.4 Fault Tolerance and Resuming from Checkpoints

Over 30 hours, process interruptions, network jitter, and resource preemption are almost inevitable. Recoverability therefore has to be a first-class requirement:

• State snapshots are written to object storage at regular intervals.
• The task orchestration layer drives retries through a message queue.
• The state hash ensures idempotency.

Any intermediate artifact must be able to be rebuilt on its own, without relying on the context.

4. Applying It to Software Engineering: Replicating the Feedback Loop in Real Projects

Formal mathematics is a special case because it comes with a perfect automated arbiter. Whether software engineering can replicate this model depends on whether you can construct an equally reliable verification signal for the task.

Large-scale software migration is the closest real-world scenario. It covers tasks such as major framework version upgrades, module boundary refactoring, and interface contract standardization. This kind of work is mechanical, high in volume, highly repetitive in pattern, and naturally comes with multiple layers of verification: compilation, unit tests, contract tests, and static analysis.

while repo.has_failing_checks():
    diff   = planner.next_step(repo.state, task_spec)          # generate the next batch of changes
    result = sandbox.apply_and_run(
                 diff,
                 checks = [compile, unit_test, contract_test, static_analysis]
             )
    if result.passed:
        memory.commit(diff, evidence = result.logs)            # commit only validated changes
    else:
        memory.recall_failures(result.logs)                    # failure samples shrink later search
    budget.accounting(result)

One rule here is non-negotiable: changes that have not passed automated verification must not enter the memory store. The biggest risk for a long-horizon agent is discovering an error only after tens of hours. By then, the cost of rework is already hard to bear. Compressing the verification cycle from hours to minutes is the core lever that determines whether long-horizon tasks can scale.

5. Cost Control: Making Long-Horizon Tasks Converge Within Budget

The cost structure of long-horizon tasks is completely different from that of traditional API calls. The per-call price matters less than the cost per unit of effective progress. Practical strategies include:

1. Tiered model routing: use strong reasoning models for high-level planning and blueprint generation. Use lightweight models for the large volume of low-value work, such as state evaluation and log classification, and bring in more powerful models only at key decision points.
2. Request caching and batching: route repeated state checks through a cache. Group verification tasks that have no interaction requirements into batched, asynchronous jobs that run on off-peak resources.
3. Timeout and budget circuit breakers: set separate limits on wall-clock time, tokens, and attempts for each task, node, and strategy branch. When a limit is exceeded, downgrade or stop the run so that a single branch cannot consume the entire budget.
4. Optional accelerated tiers: some platforms offer a fast mode that provides higher throughput at a higher price per unit. For search-type tasks, higher throughput often shortens wall-clock time enough to offset the price increase. Enable it based on measured “effective progress per hour” rather than intuition.
5. Observability first: track metrics such as “validated changes per hundred verification attempts,” “average number of retry rounds,” and “budget consumption over time,” and connect them to alerting. Without these metrics, tuning long-horizon tasks is pure guesswork.

6. Deployment Architecture: A Layered Design

In production, a long-horizon agent usually needs four decoupled layers:

• Orchestration layer: handles task decomposition, DAG scheduling, budget allocation, and priority preemption.
• Execution sandbox layer: containerized, isolated environments that provide compile, test, and run capabilities while restricting network and file system access.
• State storage layer: object storage holds artifacts and snapshots, a relational or key-value store maintains the state index and deduplication table, and a message queue handles task distribution and retries.
• Observability layer: a log service aggregates execution traces, and monitoring and alerting cover cost, success rate, and abnormal termination.

On general-purpose cloud platforms such as Baidu AI Cloud, these four categories map to standard building blocks: container platforms, object storage, message queues, log services, and monitoring and alerting. You can combine them as needed without depending on a single proprietary component. In practice, deploy the verifier and the generator in separate resource pools. Apply strict least-privilege controls to the verifier’s execution environment so that incorrect output from the generator cannot gain execution permissions.

7. Risks and Boundaries: What the Enthusiasm Should Not Overshadow

• Correctness of the verifier itself: the trustworthiness of the whole approach depends entirely on the proof kernel or the test suite. If the kernel’s assumptions differ from real mathematical intuition (for example, because a different axiom system was chosen), a gap can remain between “formalization complete” and “mathematically true.” For key results, keep a human review step.
• Incomplete test signals: passing automated checks in software engineering does not mean the semantics are correct. Code coverage does not equal behavioral equivalence. This matters most for concurrency, timing, and external dependencies, where missing signals can let an agent push confidently in the wrong direction for hours.
• The need for tiered safety guardrails: once a model with strong autonomous execution capabilities is given access to real build, deployment, and data processing systems, its risk surface is far larger than that of text generation. Assign permissions by capability domain and audit outbound activity. High-risk operations (production writes, permission changes, data deletion) should still require human confirmation.
• Benchmark contamination and overgeneralization: success on a single task does not extend directly to every domain. The real level of long-horizon capability should be measured by a stable pass rate on unseen, automatically verifiable, cross-domain task sets.

8. Conclusion

The real engineering significance of this case is not that “AI can do math now.” It is that when the feedback signal is reliable enough, state management is solid enough, and budget limits are clear enough, autonomous agents can operate stably on time scales of tens of hours.

For developers, only three lessons carry over:

• Find a correctness signal that a machine can adjudicate.
• Move state out of the context into external storage, and add deduplication and checkpoint recovery.
• Account for cost per unit of effective progress rather than per call.

With these three in place, long-horizon agents stop being a spectacle from demo videos. They become real engineering roles that can join CI pipelines and take on migrations and refactoring.