1. Set the fact boundary first: this is a claim, not a verified result

The claim circulating online is that when a vendor released its latest general-purpose large model, it said the model produced a machine-checkable formalization of Fermat’s Last Theorem in about 30 hours, and simultaneously claimed it had completed a large-scale cross-language migration of a major codebase, designed working electronic devices, and posted a large jump on simulated robotic manipulation benchmarks.

As of this writing, I have no first-hand material that can be independently verified. By normal engineering practice, judging whether such a claim is credible comes down to four things:

1. Publisher and version. Which organization, which model version, which release date.
2. Executable artifacts. The proof-script repository, the versions of the mathematical libraries it depends on (for example, a Lean/Mathlib tag or commit hash), and the checker version.
3. Scope of the formalization. A full proof, or a proof skeleton, tactic-search output, or a large number of sorry placeholders plus lifting of existing library results.
4. Human intervention record. How many lemmas were given their ideas or code by a person, with the model only completing the work.

Any performance numbers, price tiers, or safety policy details cited below are “as claimed in the release material.” I have not verified them independently. When doing technical selection, treat them as hypotheses awaiting verification, not design baselines.

2. Why formal proof is hard: it is not “proving truth,” it is “writing code that passes the checker”

Interactive theorem provers built on dependent type theory and the Curry–Howard correspondence impose hard constraints:

• Propositions are types, proofs are programs. There is nowhere to hide vague reasoning; a proof is a term that type-checks.
• No skipping steps. Every “obviously follows” or “by a similar argument” from a paper must be expanded. Formalization effort is typically 5–20× the length of the paper.
• Feedback is cheap but strict. The checker replies only “pass/fail plus error locations” and gives no hints. This is the friendliest signal source for automation, and also where models are most prone to local patching while drifting globally.
• Dependencies form a DAG, not a linear chain. Thousands of lemmas form a directed acyclic graph; changing one upstream definition breaks everything downstream at once.

So the real bottleneck is the search space and the verification loop, not compute. Three factors decide whether the task finishes: candidate tactics explode combinatorially, a single tactic needs multiple rounds of error feedback to converge, and upstream changes trigger large-scale rework.

3. How to do it: turn “one big goal” into “a set of small verifiable goals”

The main loop looks like this (the interfaces below are illustrative, not runnable code: model, checker, retrieve_context, and escalate_to_human must be replaced with your own dependencies and implementations):

# Schematic main loop for a formalization / large-scale refactor agent (not runnable as-is)
LEMMAS = load_lemma_dag(spec)      # Dependency graph: theorem -> lemmas -> existing math library
queue = topo_sort(LEMMAS)          # Topological order; leaf goals with no open dependencies first
verified = {}                      # Persistent cache of verified results (artifact store)
while queue:
    goal = queue.pop()
    if goal in verified:
        continue
    ctx = retrieve_context(goal, top_k=8)   # Recall definitions, existing lemmas, similar proof patterns
    for attempt in range(MAX_RETRY):
        script = model.generate(goal, ctx)        # Generate candidate proof script
        result = checker.verify(script)           # The only trustworthy reward signal
        if result.ok:
            verified[goal] = script               # Store the intermediate result for downstream reuse
            invalidate_downstream(goal)           # Invalidate affected upstream/downstream results
            break
        ctx = ctx + parse_diagnostics(result.errors)  # Feed errors back in as context
    else:
        escalate_to_human(goal)                   # Split the proposition / switch strategy / human takeover

Five design decisions determine success:

• The verifier is the reward. Never substitute “another model scores it” for the real checker. The task domain must provide a deterministic, cheap, ungameable acceptance signal.
• Intermediate results must be turned into artifacts. A multi-hour run will inevitably hit a context limit; only when verified lemmas are persisted as retrievable artifacts does the job become resumable.
• Fan out in parallel. Leaf lemmas with no dependencies can be dispatched in batches to many workers. This is the main reason “weeks of human labor” can compress into “tens of hours of machine time.”
• Classify failures and define escalation paths. Distinguish strategy errors (change approach), missing dependencies (supply upstream work), and over-strong goals (split the proposition), rather than retrying blindly and burning budget.
• Humans only set goals and adjudicate. Proposition decomposition, choice of abstraction level, and fallback on nodes that repeatedly fail.

4. How to choose: task domain × acceptance signal × human gate × cost factor

Task domain	Deterministic acceptance signal	Recommended human gate	Main cost factor
Formal proof	Checker pass/fail plus error locations	Lemma splitting, abstraction level, sorry audit	Number of lemmas × retry rounds × tokens per script
Cross-language code migration	Unit tests, compilation, behavioral diff	Public API compatibility, production changes	Repository size × depth of dependencies
Hardware/RTL design	Simulation passes, timing closure at synthesis	Physical constraints, reliability review	Number of design items × simulation rounds
Desktop/browser automation	End-to-end task success rate	Production write operations, outbound data	Step count × recovery attempts
Simulated robot manipulation	In-simulator success rate (not on real hardware)	Sim-to-real validation, safety testing	Episode count × environment concurrency
Open-domain writing/analysis	No deterministic signal	Human review end to end	Mostly human labor; be cautious about automation

The rule in one sentence: if a task has no deterministic acceptance signal, it is not a good fit for long-horizon agents today.

5. How to estimate cost: use a formula, not a unit-price negotiation

The release material reportedly offers both a speed improvement and an optional “fast mode” that trades a higher unit price for higher generation speed. I cannot verify the specific price tiers, billing units, currencies, or validity periods, so I do not quote numbers here. Instead, here is an illustrative cost model:

Total cost ≈ Σ(subtasks) [ unit token price × (input tokens + output tokens) × average retry rounds ]
           + fallback human hours × labor rate
           + verification infrastructure (checkers / simulation clusters / queues)

Two criteria follow:

1. Pick a tier by task type. For offline batch work (large-scale migration, regression audits, document generation), use the base tier and get throughput from concurrency. For interactive completion and real-time agent loops, latency matters; the premium for a faster tier is usually covered by the engineering time it saves.
2. Compute total cost of ownership before unit price. If average retries drop from three rounds to 1.5, a faster tier at double the unit price can still be cheaper. Improving the hit rate of the verification loop often beats negotiating a lower unit price.

Also note that long-term subscriptions and quota resets are industry practice — effectively trading retention for amortized marginal cost. Do not count promotional quota as stable capacity when planning.

6. How to evaluate: avoid the “benchmark-chasing illusion”

• Move from “snippet completion” to “repository-level / environment-level.” Single-function benchmarks say nothing about long-horizon performance.
• Look at closed-loop success rate, and at variance. The release reportedly claims simulated manipulation success rose from 27.6% to 64.9% — this figure comes from the release material; the test set, the definition of success, the sample size, and the statistical method were not disclosed, so it should not drive a selection decision. What you should measure yourself is pass@k and the cost distribution: “passes on the first run” and “passes eight of ten runs” are completely different in usability. Also watch for the sim-to-real gap.
• Watch for data contamination. Public problems easily end up in training corpora, inflating closed-book scores; open-ended tasks with tools and checkers resist contamination better.
• Common mistakes list: evaluating only on single functions; looking at the mean and ignoring variance; using model scoring instead of a checker; ignoring training-data contamination; treating simulation success rate as real-hardware success rate; counting sorry as completed.

7. Safety tiering: only reusable process principles

According to the release material, the general version ships with stricter network and biosecurity guardrails, is open to all users, and requires a dedicated application plus organizational purpose review for sensitive research directions. I cannot verify the publisher, version, applicable regions, or review basis, so I will not detail unverified specifics. What transfers:

• Capability should not split because of safety policy. Implement guardrails as a policy layer before and after inference (intent classification, domain refusals, audit trails) rather than as a capability reduction at training time, so you do not maintain two models.
• Sensitive capabilities follow an “apply — review — restrict — audit” loop. Access control, purpose declarations, and log retention should be process, not verbal agreement.
• Guardrails must be testable. Keep an adversarial red-team set for high-risk intents plus a regression pipeline, and rerun both on every model or policy update.

8. Production checklist: seven steps to production

1. Verification first. Confirm the target domain has a deterministic acceptance signal. If it does not, do not start.
2. Make intermediate results artifacts. Push verified lemmas, migrated modules, and passing patches into object storage and version control as retrievable context and resume checkpoints.
3. Elastic execution layer. Scale parallel workers on demand with a container platform; pool burst work separately from everyday interactive work to avoid contention.
4. Full-chain observability. Instrument generation, verification, retries, and human escalation; track success rate, retry rate, per-task cost, and tail latency.
5. Asynchronous task queue. Decouple long-running jobs with a message queue, with failure requeue, priority scheduling, and idempotent reruns.
6. Human gates. Require mandatory human review for production changes, outbound data, and sensitive-domain output.
7. Pilot before scaling. Start with a mid-sized scenario that has clear boundaries and an explicit acceptance criterion (for example, migrating one module across languages, or formalizing a core algorithm’s specification). Prove the “decompose — parallelize — verify — cache” loop, then expand.

9. FAQ

Q: How exactly do you approach formalization?
Pin the proof assistant and math library versions first, decompose the human proof into a lemma DAG, then run the “generate candidate script → verify with checker → feed errors back” loop on each leaf lemma, committing every lemma that passes immediately.

Q: How do you choose a framework for long-horizon agents?
Only three things matter: whether a pluggable deterministic verifier exists, whether intermediate results can be persisted and resumed from a checkpoint, and whether failure classification and escalation are supported. Missing any one, the framework is unsuitable for long tasks.

Q: How do you estimate cost?
Use the formula in the previous section, treat retry rounds as the main variable, measure the retry rate on a small scale before extrapolating, and do not build a total budget directly from a launch-event unit price.

Q: What must not be automated?
Proposition decomposition and choice of abstraction level, production write operations, outbound data in sensitive domains, and sim-to-real validation. These must be covered by humans.

Conclusion: Even if “formalizing Fermat’s Last Theorem in 30 hours” is never independently verified, the methodology stands: cut an unverifiable large goal into verifiable small ones, replace subjective evaluation with a deterministic verifier, persist intermediate results to fight context loss, compress time with parallel fan-out, and constrain scale with tiered guardrails and a cost model. What you can start preparing today is your own verification infrastructure.