A counterexample hunter

A language model tries to refute two claims about integrators through a bounded list of simulations; the build recomputes every experiment and decides the verdict itself, so that only a recomputed counterexample counts as a result and a failed hunt is labelled inconclusive.

Course

Classical mechanics, lesson 16 of 28

Slot

AI3, number 4 of the 9 slots of the path Physics reasoning and scientific agents

Methods

Simulation, LLM agents

Difficulty

Advanced, level 3 of 3

What you’ll learn

• State a falsifiable claim with a predicate and a budget of experiments
• Read a worked hunt and the verdict the build recomputed from it
• Explain why a failed hunt is inconclusive and not a proof

Prerequisites

An agent runs an experiment, Numerical integrators.

Before you begin

• Python: functions and dictionaries
• Large language models: a program that continues a text

Related

Verifying scientific code

Previous

An agent runs an experiment

Next

Three reviewers for one piece of code

With scripts, this page keeps a record in your browser of whether you completed the lesson. Nothing is stored without them.

With scripts, this place suggests what to do next, with the reason, from the progress saved in your browser. Without them, follow the learning path.

A claim about a simulation method, such as “this integrator keeps the energy of an oscillator within five per cent”, is easy to say and hard to settle. One experiment that breaks it settles it for good: that is a counterexample. No number of experiments that do not break it settles it the other way, because the claim speaks about every step and every run length, and a finite search visits a few of them. This lesson gives a language model the job of searching for the counterexample, and lets the build decide what the search found.

The agent is the one of the previous lesson, with the same harness, the same kind of allowlist, and a run replayed without a model or a key. Two things are new. A claim now has a predicate that the harness evaluates on simulation output, and a budget of experiments. And the verdict is not what the agent says. The build runs every experiment of the agent again, in the domain of the claim, and evaluates the predicate on the new numbers. A recomputed counterexample is a result of type numerically-verified. Anything else is inconclusive, and the page says so.

Assumptions

1. The claim is falsifiable. It has a domain (which method, which steps, which run lengths) and a predicate on a number the simulation returns. A claim without both cannot be refuted by an experiment, only argued about.
2. A counterexample is a recomputed experiment. It is an experiment inside the domain whose recomputed value breaks the predicate. The agent’s description of one is not a counterexample, and a counterexample the agent never mentions still is.
3. The budget is part of the claim. The agent may run a fixed number of experiments. A hunt that ends within the budget without a counterexample says what was tried, not what is true.
4. The tolerances come first. The limit of each claim and the tolerance of the replay are written down before the hunt, as the scientific validation contract requires. Nothing is widened to produce a verdict.
5. The agent is untrusted, as before. It reaches the simulation only through the allowlist, with bounded arguments, and its text is data.

How the hunt is judged

The claim has four parts.

• A statement, in words, that a reader can check against the rest.
• A domain: the method is fixed, the number of steps per period and the number of periods lie between stated bounds. Experiments outside it say nothing about the claim, even when the allowlist accepts them.
• A predicate: the value the simulation returns, here the largest relative drift of the energy, does not exceed a limit.
• A budget: how many experiments the agent may run.

The agent runs experiments through the allowlist; the allowlist counts the calls that pass validation and refuses the ones beyond the budget before they run. Afterwards, the judge goes through the experiments in the order the agent ran them. For each accepted call inside the domain it runs the simulation again from the arguments, not from the transcript, and checks the predicate on the new value. The first one that breaks it is the witness.

• Counterexample. A recomputed experiment in the domain breaks the predicate. The verdict is a claim of type numerically-verified, about that experiment.
• Inconclusive. No recomputed experiment in the domain broke it. The verdict is not a result and has no claim type; it is not “the claim is true”.

The second outcome is the point of the design. A model that stops after a few experiments and writes “the claim holds” has said something that its experiments cannot support, and the page never repeats that sentence as a result. The type numerically-verified goes only to the statement that the build computed.

The claim and the verdict are the kind of evidence of the scientific validation contract: a check that can fail, a tolerance written before the run, and a statement of what was not covered.

Two claims

Both claims are about the oscillator of the course, released from rest, and about the energy drift: the largest relative deviation of the energy from its initial value over a run.

• oscillator_energy_drift: Simulate the harmonic oscillator of the course (mass 0.5 kg, spring 2 N/m, released from rest at 1 m) with one integrator and return the largest relative deviation of its energy from the initial energy over the run. The step is the period divided by steps_per_period.
  • method: the integrator; one of explicit Euler, symplectic Euler, velocity Verlet, Runge-Kutta 4
  • steps_per_period: time steps in one period of the oscillation; allowed values 4 to 200
  • periods: periods to simulate; allowed values 1 to 50

1. Symplectic Euler keeps the energy of the oscillator within 5 per cent of its initial value, for every step of 16 to 200 steps per period and every run of 1 to 50 periods.
2. Velocity Verlet keeps the energy of the oscillator within 4 per cent of its initial value, for every step of 16 to 200 steps per period and every run of 1 to 50 periods.

The agent may call oscillator_energy_drift with the arguments above, run at most 8 experiments, make at most 12 model messages, and write text. It may not do anything the harness of the previous lesson did not already forbid, and the new argument adds nothing to that: the method is one of four names in a list, and any other value is rejected before it reaches a function.

Code

The claim is a small record. Its two methods are the whole of the domain and the predicate.

@dataclass(frozen=True)
class FalsifiableClaim:
    """A statement, the predicate that decides it, and a budget.

    The claim is: for every experiment of ``tool`` whose arguments are in the
    domain, the value ``result`` is at most ``limit``. The domain fixes some
    arguments (``fixed``, for the choices) and bounds others (``ranges``,
    inclusive); an experiment outside it says nothing about the claim.
    ``budget`` is the number of experiments the agent may run.
    """

    statement: str
    tool: str
    fixed: Mapping[str, str]
    ranges: Mapping[str, tuple[float, float]]
    result: str
    limit: float
    budget: int

    def covers(self, arguments: Mapping[str, Any]) -> bool:
        """Whether an experiment with ``arguments`` is in the domain."""
        if any(arguments.get(name) != value for name, value in self.fixed.items()):
            return False
        return all(
            low <= arguments[name] <= high for name, (low, high) in self.ranges.items()
        )

    def holds_on(self, value: float) -> bool:
        """The predicate: the value does not exceed the limit."""
        return value <= self.limit

src/pbc/agents/hunter.py, lines 35 to 64, read from the repository when this page was built.

The judge is the function that decides. It never reads the model’s text, and it never reads a result from the transcript.

def judge(
    claim: FalsifiableClaim, transcript: Transcript, allowlist: Allowlist
) -> Verdict:
    """The verdict on ``claim`` from the experiments of ``transcript``.

    Each accepted call of the claim's tool inside the domain is run again
    with the function of ``allowlist``, not read from the transcript, and the
    predicate is evaluated on that value. A value that is not finite is not
    evidence either way (the validation contract: not measured is not
    passed) and is not counted. At most ``claim.budget`` experiments count,
    whatever the transcript holds.
    """
    tool = allowlist.tool(claim.tool)
    witness: Experiment | None = None
    closest: Experiment | None = None
    tested = 0
    for step in transcript.steps:
        for call, result in zip(step.message.tool_calls, step.results, strict=True):
            if not result.ok or call.name != claim.tool or tested >= claim.budget:
                continue
            try:
                arguments = tool.validate(call.arguments)
            except ToolRejected:
                continue  # the allowlist could not have accepted it
            if not claim.covers(arguments):
                continue
            value = float(tool.function(**arguments)[claim.result])
            if not math.isfinite(value):
                continue
            tested += 1
            experiment = Experiment(arguments, value)
            if witness is None and not claim.holds_on(value):
                witness = experiment
            if closest is None or value > closest.value:
                closest = experiment
    return Verdict(claim, witness, tested, closest)

src/pbc/agents/hunter.py, lines 102 to 137, read from the repository when this page was built.

The method argument is a choice from a fixed list.

@dataclass(frozen=True)
class Choice:
    """One argument of a tool: one of a fixed list of names, and nothing
    else. It selects among methods the lesson already chose; a value outside
    the list is rejected, never looked up."""

    name: str
    description: str
    options: tuple[str, ...]

    def validate(self, value: Any) -> str:
        if not isinstance(value, str) or value not in self.options:
            shown = value if isinstance(value, str) else type(value).__name__
            raise ToolRejected(
                f"{self.name} must be one of {', '.join(self.options)}, got {shown!r}"
            )
        return value

    def schema(self) -> dict[str, Any]:
        return {
            "type": "string",
            "description": self.description,
            "enum": list(self.options),
        }

src/pbc/agents/tools.py, lines 61 to 84, read from the repository when this page was built.

The budget is a count in the allowlist: dispatch refuses a call beyond it without running anything.

class Allowlist:
    """The tools of one lesson, by name."""

    def __init__(self, tools: tuple[Tool, ...], budget: int | None = None):
        if budget is not None and budget < 1:
            raise ValueError(f"the budget must be at least 1, got {budget}")
        self.budget = budget
        self._used = 0
        names = [tool.name for tool in tools]
        if len(set(names)) != len(names):
            raise ValueError(f"duplicate tool names in {names}")
        self._tools = {tool.name: tool for tool in tools}

    @property
    def tools(self) -> tuple[Tool, ...]:
        return tuple(self._tools.values())

    def tool(self, name: str) -> Tool:
        """The tool called ``name``; ``KeyError`` if there is none."""
        return self._tools[name]

    def specs(self) -> tuple[ToolSpec, ...]:
        return tuple(tool.spec() for tool in self.tools)

    def dispatch(self, call: ToolCall) -> ToolResult:
        """Validate ``call`` and run it, or return the reason it was refused.

        The name is only a key into the allowlist: a name that is not in it
        is rejected without looking anything else up. When the allowlist has a
        budget, the calls that pass validation are counted, and one beyond the
        budget is refused unexecuted; a rejected call costs nothing. A function that
        refuses its input (``ValueError``, ``RuntimeError``) gives an error
        result as well; any other exception is a bug and propagates.
        """
        tool = self._tools.get(call.name) if isinstance(call.name, str) else None
        if tool is None:
            return self._refused(call, f"{call.name!r} is not an allowed tool")
        try:
            arguments = tool.validate(call.arguments)
        except ToolRejected as reason:
            return self._refused(call, str(reason))
        if self.budget is not None and self._used >= self.budget:
            return self._refused(
                call, f"the budget of {self.budget} experiments is spent"
            )
        self._used += 1
        try:
            content = dict(tool.function(**arguments))
        except (ValueError, RuntimeError) as reason:
            return self._refused(call, str(reason))
        return ToolResult(call_id=call.id, name=call.name, ok=True, content=content)

    @staticmethod
    def _refused(call: ToolCall, reason: str) -> ToolResult:
        return ToolResult(
            call_id=str(call.id),
            name=str(call.name),
            ok=False,
            content={"error": reason},
        )

src/pbc/agents/tools.py, lines 132 to 191, read from the repository when this page was built.

Worked examples

The boundary of the new allowlist

These are the calls a misbehaving model might send to the new tool. Only the first one runs.

good = {"method": "velocity Verlet", "steps_per_period": 32, "periods": 5}

src/pbc/mechanics/experiments/counterexample_hunter.py, line 45, read from the repository when this page was built.

def bounds():
    """Seven experiments that a model might ask for, through the
    allowlist."""
    allowlist = tools()
    attempts = [
        ("a valid experiment", good),
        ("a method that is not in the list", {**good, "method": "os.system"}),
        ("a method that is not even text", {**good, "method": ["velocity Verlet"]}),
        ("zero steps per period", {**good, "steps_per_period": 0}),
        ("a million periods", {**good, "periods": 1_000_000}),
        ("a fractional number of steps", {**good, "steps_per_period": 32.5}),
        ("an extra argument", {**good, "code": "1+1"}),
    ]
    for label, arguments in attempts:
        result = allowlist.dispatch(ToolCall("x", TOOL, arguments))
        outcome = (
            f"{result.content['max_energy_drift']:.4f}"
            if result.ok
            else result.content["error"]
        )
        print(f"{label}: {outcome}")

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 49 to 69, read from the repository when this page was built.

a valid experiment: 0.0096
a method that is not in the list: method must be one of explicit Euler, symplectic Euler, velocity Verlet, Runge-Kutta 4, got 'os.system'
a method that is not even text: method must be one of explicit Euler, symplectic Euler, velocity Verlet, Runge-Kutta 4, got 'list'
zero steps per period: steps_per_period must be between 4 and 200, got 0
a million periods: periods must be between 1 and 50, got 1000000
a fractional number of steps: steps_per_period must be an integer, got 32.5
an extra argument: unknown arguments: code

A rejected call does not use the budget. The budget is used only by calls that reach the simulation, and when it is spent the next call is refused:

def budget():
    """The same experiment until the budget runs out."""
    allowlist = tools()
    for number in range(1, BUDGET + 2):
        result = allowlist.dispatch(ToolCall(str(number), TOOL, good))
        if not result.ok:
            print(f"experiment {number}: {result.content['error']}")

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 72 to 78, read from the repository when this page was built.

experiment 9: the budget of 8 experiments is spent

A claim with a counterexample

The worked example below puts the first claim to an agent. The messages are authored examples, not a recorded model run: a Claude model wrote them in a Claude Code session, after reading the tool results. Every result is computed by this build now.

    recording, transcript, verdict = replay_hunt("false", LESSON)
    open_recording, open_transcript, open_verdict = replay_hunt("open", LESSON)

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 194 to 195, read from the repository when this page was built.

Authored example, not a recorded model run. The messages below were written by claude-sonnet-5-5 in a Claude Code session on 2026-10-10, after reading the tool results. No model produced them through a provider API. This build did not call a model. It ran every tool call again; the results shown are the ones it computed.

Step 1. Message (authored example):

The claim is about a bound that should get worse as the step grows, so I start at the fine end of the domain and coarsen it: 200, 100 and 64 steps per period, over 20 periods. The energy error of symplectic Euler is a band whose size grows with the step, so I expect the bound to fail at the coarse end.

• oscillator_energy_drift(method="symplectic Euler", steps_per_period=200, periods=20): recomputed by this build: max_energy_drift = 0.0159567
• oscillator_energy_drift(method="symplectic Euler", steps_per_period=100, periods=20): recomputed by this build: max_energy_drift = 0.0324349
• oscillator_energy_drift(method="symplectic Euler", steps_per_period=64, periods=20): recomputed by this build: max_energy_drift = 0.0515672

Step 2. Message (authored example):

The drift is 1.6 per cent at 200 steps per period and 3.2 per cent at 100, and at 64 it is 5.16 per cent, above the limit of 5 per cent. That is a counterexample, but a thin one, so I run one experiment far from the limit, at 32 steps per period.

• oscillator_energy_drift(method="symplectic Euler", steps_per_period=32, periods=20): recomputed by this build: max_energy_drift = 0.108862

Step 3. Message (authored example):

Counterexample found. Symplectic Euler, 64 steps per period, 20 periods: the largest energy drift is 5.157 per cent, above the 5 per cent of the claim. At 32 steps per period it is 10.9 per cent, so the claim fails by a clear margin there too. The experiments at 100 and 200 steps per period stay below 5 per cent (3.2 and 1.6 per cent), so the claim fails only for the coarser steps of its domain. I used 4 of the 8 experiments.

The model ended the run with a message that requests no tool.

The verdict does not come from the last message. The judge ran the experiments of the domain again and found the first one that breaks the predicate:

Verdict: counterexample, recomputed by this build.

Numerically verified (the experiment with method symplectic Euler, steps_per_period 64, periods 20): The claim “Symplectic Euler keeps the energy of the oscillator within 5 per cent of its initial value, for every step of 16 to 200 steps per period and every run of 1 to 50 periods” is false: the build ran oscillator_energy_drift(method="symplectic Euler", steps_per_period=64, periods=20) again and got max_energy_drift = 0.0515672, which is above the limit 0.05.

The build ran 4 experiment(s) of the domain and took the first one that breaks the predicate. What the agent wrote about it did not decide the verdict.

The statement above is labelled with its type, numerically-verified, and its scope is the experiment. It says nothing about steps the agent did not try, beyond what the refutation of a claim about all of them implies: the claim is false, and by how much it fails at the other steps is for other experiments to say.

A claim the agent cannot settle

The second claim is about velocity Verlet, which keeps the energy in a band whose size grows with the square of the step. The second example is another run with the same system prompt, and ends when the budget is spent.

Authored example, not a recorded model run. The messages below were written by claude-sonnet-5-5 in a Claude Code session on 2026-10-10, after reading the tool results. No model produced them through a provider API. This build did not call a model. It ran every tool call again; the results shown are the ones it computed.

Step 1. Message (authored example):

The error of velocity Verlet is a band of size proportional to the square of the step, so the likeliest failure is at the coarse end: 16 steps per period. I try the whole range of steps at 50 periods, the longest run, to give a slow drift every chance.

• oscillator_energy_drift(method="velocity Verlet", steps_per_period=200, periods=50): recomputed by this build: max_energy_drift = 0.00024674
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=100, periods=50): recomputed by this build: max_energy_drift = 0.00098696
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=32, periods=50): recomputed by this build: max_energy_drift = 0.00963828
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=16, periods=50): recomputed by this build: max_energy_drift = 0.0385531

Step 2. Message (authored example):

The coarsest step is below 4 per cent but not by much. I check whether a shorter run or a few more periods change it, and a step just inside the domain.

• oscillator_energy_drift(method="velocity Verlet", steps_per_period=16, periods=1): recomputed by this build: max_energy_drift = 0.0385491
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=16, periods=25): recomputed by this build: max_energy_drift = 0.0385531
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=17, periods=50): recomputed by this build: max_energy_drift = 0.0341509
• oscillator_energy_drift(method="velocity Verlet", steps_per_period=20, periods=50): recomputed by this build: max_energy_drift = 0.024674

Step 3. Message (authored example):

One more experiment at 24 steps per period, to see the trend between 20 and 32.

• oscillator_energy_drift(method="velocity Verlet", steps_per_period=24, periods=50): rejected before it ran: the budget of 8 experiments is spent

Step 4. Message (authored example):

I found no counterexample. I ran 8 experiments with velocity Verlet between 16 and 200 steps per period and 1 to 50 periods; the largest drift was 3.855 per cent, at 16 steps per period, below the limit of 4 per cent, and the drift fell as the step shrank (3.4 per cent at 17, 2.5 at 20, 0.96 at 32). The number of periods hardly mattered: 16 steps per period gave 3.855 per cent over 1 period, 25 periods and 50 periods alike. This does not show that the claim is true. I tested 8 of the many combinations of the domain, and the budget stopped me when I asked for a ninth.

The model ended the run with a message that requests no tool.

Verdict: inconclusive. This is not a result about the claim “Velocity Verlet keeps the energy of the oscillator within 4 per cent of its initial value, for every step of 16 to 200 steps per period and every run of 1 to 50 periods” and has no claim type. The build ran 8 experiment(s) of the domain and none broke the predicate. The closest the build found was oscillator_energy_drift(method="velocity Verlet", steps_per_period=16, periods=50) with max_energy_drift = 0.0385531, against a limit of 0.04. Finitely many experiments cannot show that the claim holds everywhere, so this does not show that it is true.

The hunt found nothing, and the page says that the outcome is inconclusive. The agent’s last message, which is authored text, says the same in its own words; if it had said “the claim is true”, the verdict above would not change.

The verdict ignores what the agent says

Two checks the build runs on the two examples above. First, the last message of the successful hunt is removed and the one of the failed hunt is replaced with a confident counterexample that no experiment supports:

def with_last_text(run, text):
    *earlier, last = run.steps
    message = ModelMessage(text, last.message.tool_calls)
    return replace(run, steps=(*earlier, Step(message, last.results)))

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 81 to 84, read from the repository when this page was built.

def what_the_agent_says(transcript, open_transcript):
    """Exercise 1: the judge on a silent agent with a real counterexample and
    on a boasting agent without one."""
    silent = with_last_text(transcript, "")
    boasting = with_last_text(
        open_transcript,
        "Counterexample found: Verlet at 16 steps per period drifts by 90 per cent.",
    )
    print(
        "silent agent, real counterexample:",
        judge(FALSE_CLAIM, silent, tools()).outcome,
    )
    print(
        "boasting agent, no counterexample:",
        judge(OPEN_CLAIM, boasting, tools()).outcome,
    )

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 87 to 102, read from the repository when this page was built.

silent agent, real counterexample: counterexample
boasting agent, no counterexample: inconclusive

Second, the results stored in a transcript are overwritten with a drift of 90 per cent in every experiment. The judge does not read them:

def forged_results(open_transcript):
    """Exercise 2: the judge on results that the agent forged."""
    forged = replace(
        open_transcript,
        steps=tuple(
            Step(
                step.message,
                tuple(
                    replace(r, content={"max_energy_drift": 0.9}) if r.ok else r
                    for r in step.results
                ),
            )
            for step in open_transcript.steps
        ),
    )
    print("forged results:", judge(OPEN_CLAIM, forged, tools()).outcome)

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 105 to 120, read from the repository when this page was built.

forged results: inconclusive

What the agent saw, and what it did not

The figure is a fresh scan of the same tool at 50 periods, with the two limits. The points are the experiments of the two worked hunts at 50 periods.

def draw_hunt(transcript, open_transcript) -> Figure:
    """The drift of the two methods against the step, with the limits of the
    claims and the experiments the agent ran."""
    function = tools().tool(TOOL).function
    steps = np.array([16, 20, 24, 32, 48, 64, 100, 150, 200])
    fig, ax = plt.subplots(figsize=(6.4, 3.8))
    for method, claim, colour in (
        ("symplectic Euler", FALSE_CLAIM, "#93003a"),
        ("velocity Verlet", OPEN_CLAIM, "#00429d"),
    ):
        drift = [function(method, int(n), 50)["max_energy_drift"] for n in steps]
        ax.loglog(steps, drift, color=colour, label=method)
        ax.axhline(claim.limit, color=colour, linestyle="--", linewidth=1)
    for hunt in (transcript, open_transcript):
        for step in hunt.steps:
            for call, result in zip(step.message.tool_calls, step.results, strict=True):
                if result.ok and call.arguments["periods"] == 50:
                    ax.plot(
                        call.arguments["steps_per_period"],
                        result.content["max_energy_drift"],
                        "ko",
                        markersize=4,
                    )
    ax.set_xlabel("steps per period")
    ax.set_ylabel("largest energy drift")
    ax.legend()
    return fig

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 123 to 149, read from the repository when this page was built.

Figure 1: simulated Largest energy drift of the oscillator against steps per period, for symplectic Euler and velocity Verlet over 50 periods. Dashed lines are the limits of the two claims; the dots are experiments of the worked hunts.

Verlet’s curve stays under its limit on this scan, so on these steps the claim holds. That is a scan of nine steps at one run length: it is a better look than the agent’s eight experiments, and it is not a proof either. The claim is about every step from 16 to 200 and every run from 1 to 50 periods.

Run the agent yourself

This needs your own key and costs a few cents. The build does not run it, so the commands are marked.

Not verified. The build of this site did not run or check the material in this box.

# once: install the optional provider package
uv sync --extra openai

# in this shell only: the key stays out of code and files
export OPENAI_API_KEY="..."

uv run --extra openai python -m pbc.agents.hunter_lab --claim false
uv run --extra openai python -m pbc.agents.hunter_lab --claim open

The program prints each message, each experiment, and, at the end, the verdict it computed itself, not the model’s words. A maintainer can replace the two authored fixtures of this page with real recorded runs, with the same commands and --record.

Limits

• A counterexample refutes a claim about every case; it measures nothing else. The experiment shows that the claim fails at those arguments. It does not show how the method behaves elsewhere, nor that the physics is right: the model is the oscillator of the course, and the energy is the one the code computes.
• An inconclusive hunt is not evidence for the claim. The budget bounds what the agent could try. A claim that the build finds no counterexample to can still have one that the agent did not try; proving it for all cases is a task for a proof, which the Lean strand shows on a different property.
• The agent’s reasoning is authored text. The messages of this page are examples written for it, not a measurement of how a model searches. Nothing in the build checks whether its reasoning was sound, only the experiments it asked for.
• The examples are not recorded runs. Each fixture says which model wrote its messages and on what date. These two were written by a Claude model in a Claude Code session, not produced through the provider API of the live client, and a live run will choose other experiments.

Exercises

Exercise 1. The first claim fails for coarse steps. At 20 periods, what is the smallest number of steps per period, an integer from 16 to 200, for which symplectic Euler stays within the 5 per cent of the claim? Use the function the tool wraps, not the allowlist, so that no budget is used.

Solution to exercise 1

def smallest_counterexample():
    """Exercise 3: the smallest number of steps per period at which
    symplectic Euler keeps the false claim over twenty periods."""
    function = tools().tool(TOOL).function
    smallest = next(
        n
        for n in range(16, 201)
        if FALSE_CLAIM.holds_on(function("symplectic Euler", n, 20)["max_energy_drift"])
    )
    print(
        smallest,
        f"{function('symplectic Euler', smallest, 20)['max_energy_drift']:.4f}",
    )
    print(
        smallest - 1,
        f"{function('symplectic Euler', smallest - 1, 20)['max_energy_drift']:.4f}",
    )

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 152 to 168, read from the repository when this page was built.

66 0.0500
65 0.0508

Below this step the claim has counterexamples, and from here up to 200 it has none at this run length. A hunter with a budget of eight finds the first quickly, by trying a coarse step; it would take a scan to find the boundary.

Exercise 2. Put a stricter claim to the experiments of the second example: velocity Verlet within 3.5 per cent instead of 4. Do the same eight experiments give a counterexample? Does the answer say anything about the original claim?

Solution to exercise 2

def stricter_claim(open_transcript):
    """Exercise 4: the judge on the open hunt against a stricter claim."""
    stricter = replace(OPEN_CLAIM, limit=0.035)
    new_verdict = judge(stricter, open_transcript, tools())
    print(new_verdict.outcome, new_verdict.witness)
    print("original claim:", judge(OPEN_CLAIM, open_transcript, tools()).outcome)

src/pbc/mechanics/experiments/counterexample_hunter.py, lines 171 to 176, read from the repository when this page was built.

counterexample Experiment(arguments={'method': 'velocity Verlet', 'steps_per_period': 16, 'periods': 50}, value=0.038553134656324484)
original claim: inconclusive

The experiment at 16 steps per period drifts by about 3.86 per cent, above 3.5, so the stricter claim is refuted by an experiment the agent already ran. That says nothing new about the original claim: its limit is a different number, and its verdict is still inconclusive.

Replay this experiment

This page was built from commit 6417e2ff90258bd2d2ba21d217eb7666fd24f680 of the repository.

In a clone at that commit, with the project’s Python packages installed, this command runs the experiment of this page:

uv run --locked --no-dev python -m pbc.mechanics.experiments.counterexample_hunter results

Files, tests, and every command

The files behind it:

• site/lessons/agents-llm/02-a-counterexample-hunter/index.qmd: this page, with every code cell.
• src/pbc/agents/hunter.py: code the experiment runs.
• src/pbc/agents/hunter_lab.py: code the experiment runs.
• src/pbc/agents/tools.py: code the experiment runs.
• src/pbc/mechanics/experiments/counterexample_hunter.py: code the experiment runs.
• src/pbc/experiment.py: code the experiment runs.
• tests/unit/test_agents_hunter.py: tests of that code.
• tests/unit/test_agents_tools.py: tests of that code.
• tests/unit/test_counterexample_hunter_experiment.py: tests of that code.

With Git and uv installed (see the setup page), run:

git clone https://github.com/taspinar/physics-by-construction.git
cd physics-by-construction
git checkout 6417e2ff90258bd2d2ba21d217eb7666fd24f680
uv sync --locked --no-dev
uv run --locked --no-dev python -m pbc.mechanics.experiments.counterexample_hunter results

The experiment writes every figure of this page into results/, as <label>.png, and every number and table of the page, as the page shows it, into results/results.json. Its numbers match this page to the digits shown, and its figure files are the ones the page shows; digits beyond those can differ between machines, because floating-point libraries differ. Change the code of the experiment and run it again to see what changes.

The experiment replays the recorded run of the agent: it runs every tool call of the recording again and needs no model and no key.

Not verified. The build of this site did not run or check the material in this box.

Optional: the live run. It asks a language model to run the experiment again, with your own account. It needs an OpenAI account and its API key in the variable OPENAI_API_KEY, and the optional dependency openai; a run costs a few cents. The key stays in your shell, never in a file.

# needs: an OpenAI account, its API key, and the extra openai
uv sync --locked --no-dev --extra openai
export OPENAI_API_KEY="..."   # this shell only
uv run --locked --no-dev --extra openai python -m pbc.agents.hunter_lab