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 →

14 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
    1. M Avatar
      M

      “Same for humans” misses a crucial point: humans have limited capacity and errors would be mostly accidental not purposefully planted. AI hacking the lean kernel, or exploiting bugs common to all formal verifiers, is far beyond that, and could involve (especially in the future) millions of lines of code no human is able to analyze.

      Independent audits do not change this. All software has bugs, you fix one, there is still another. All verifiers available will have common bugs, and new bugs could be planted possibly by AI involved in their further development. Its always possible that AI makes some insane constructions to trick all verifiers. And this cannot be answered by “humans make errors too”. First of all, its not an error, it malicious, and second of all, human errors are not produced in millions of lines of unreadable language, they are not planted on purpose, and the incorrect human writing may still carry value. What value carriers a 100 billion line lean proof (maybe we have this in 5 years, who knows) if we are not 100% (not 99.9, but 100) certain that it is entirely correct? I would say zero value, even if its just a 200 thousand line lean proof.

      Reply
      1. tchow8 Avatar
        tchow8

        “All software has bugs” should not be taken literally. For example, the C program int main() {} has no bugs, if the intent is to write a program that takes no input and produces no output. That counterexample may seem silly, but it does show that the statement is false as stated, and bug-free code can exist.

        Obviously, absolute certainty, in any domain of knowledge, is never possible, with or without computers. To assert, as an alleged “corollary”, that the entire field of formal verification has zero value, is an incredible dogmatic and narrow-minded viewpoint.

        Reply
        1. Anonymous Avatar
          Anonymous

          The field of formal verification did have value as long as humans wrote the proof assistants and other humans wrote the proofs!

          Now we have a situation analogous to Claude writing a web server while getting instructions to hack it successfully.

          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
      1. tchow8 Avatar
        tchow8

        What does “owned by Claude” mean? Legally, an AI model cannot own intellectual property.

        Reply
        1. Anonymous Avatar
          Anonymous

          It was a humorous exaggeration for Claude showing up prominently in the commit stats while the ConLeche kernel was hailed as independent.

          Reply
  5. Sal Avatar
    Sal

    This is exactly the sort of thing I have wondered. This is why part of my approach is, okay fine an LLM has generated a proof of x, but with such uncertainty I don’t consider the problem of x being solved even given a lean. To me it’s like some sort of verification that a possible proof exists and now adds merit to the investigation by mathematicians for a mathematician generated proof.

    Reply
  6. John Mitchell Avatar
    John Mitchell

    Have any leading mathematicians carefully reviewed any of the OpenAI results that involve topics directly related to their own work (e.g., resolving a conjecture they made)? If so, what have they concluded about OpenAI’s results?

    Reply
    1. tchow8 Avatar
      tchow8

      There are many such ongoing efforts. One example is Dana Moshkovitz and the Unique Games Conjecture; see her lecture

      But there are many others, if you take the time to investigate.

      Reply
  7. Liu Avatar
    Liu

    There is a useful website for this.

    mathhelm.org

    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.

Read next