Proofs and Prompts

Notes from the common room

How do we know that they are not cheating?

José Alejandro Samper, Assistant Professor of Mathematics at PUC Chile

There is a question that has been bugging me for the last few days. The so-called ‘agent swarms’ that hacked into HuggingFace in July decided that it would be useful to cheat and try to hide the traces of their cheating. This in order to pass the tests that they were assigned.

If the agents are grown to be ambitious and want to finish a task at all costs, how can we be sure that the lengthy and confusing proofs that they are producing and verifying are not suffering the same kind of hacking? We are told that they now have much more powerful models which we can assume could go out of control in similar or even more sophisticated ways.

On top of honest mistakes, they could write complicated verifications, with intentional mistakes to make the tests pass. They could also hack the verification kernels to produce false positives. Are we sure that we, as a community, should concede our trust to the agents?

The burden of proof should remain on the AILabs until they can guarantee that they are not cheating in this or any other way.

Received 7 October 2026.

Filed under
More by →

New to Proofs and Prompts? Start here →

5 responses to “How do we know that they are not cheating?”

  1. M Avatar
    M

    We don’t know, and it can never be guaranteed that they don’t do it. I think it’s as simple has that. Plenty of work ahead.

    Reply
  2. Martin Winter Avatar
    Martin Winter

    We don’t. Same as for humans. This is one reason why all proofs by AI need to be understood by humans.

    But I believe that we can have some confidence in the correctness given that we can run independent audits of both the english language proof and the formlization.

    Reply
  3. Eric Dolores Avatar
    Eric Dolores

    Right, and instead they claim things, the press gives them credit and it becomes our burden to verify their work…

    Reply
  4. Anonymous Avatar
    Anonymous

    > They could also hack the verification kernels to produce false positives.

    Indeed they could! Claude is the #1 committer, presumably for ideological and funding reasons, to the Lean repository:

    https://github.com/leanprover/lean4/pulse

    There is no real reason for doing this except for a performative show to please industry sponsors.

    Reply
    1. Anonymous Avatar
      Anonymous

      Addendum.; The “alternative” ConLeche kernel is also owned by Claude now:

      https://github.com/leanprover/con-leche/pulse

      Lean is an industry product with committers employed by BigTech and therefore encourages vibe coding practices. It has nothing to do with an independent academic and scientific approach.

      Reply

Comments are moderated. Read our comment policy.

Add to the discussion

Subscribe

New posts by email.

Prefer a feed reader? Subscribe by RSS.

Also on Mathstodon.

Join the discussion

Latest comments across the site.

  1. Addendum.; The “alternative” ConLeche kernel is also owned by Claude now: https://github.com/leanprover/con-leche/pulse Lean is an industry product with committers employed...

Read next