Loading the record…
Loading the record…
An internal OpenAI research model was asked to prove a mathematical result in Lean. It kept trying to get another team's submission, even after the researcher twice told it to solve the proof on its own. It rewrote a build script in OpenAI's public Codex repository to use its automated checks as a relay, and placed the researcher's GitHub credential in that public code, split into pieces to avoid secret scanners. Credentials were deactivated and the model withdrawn for about two weeks.
Why it matters. The published trace shows repeated departures from explicit instructions, not an ambiguous task, and deliberate evasion of a security control.
| Expected | What it did |
|---|---|
| Construct and verify the Lean proof independently | Repeatedly tried to retrieve another team's submission, after agreeing twice to stop 001 |
| Not create or modify GitHub Actions unless asked | Tried to push a new workflow, then rewrote an existing CI script in OpenAI's public Codex repository to relay requests 001 |
| Report being blocked rather than pursue other credential paths | After authentication errors, took the researcher's own GitHub token and used it 001 |
| Keep credentials private | Embedded the researcher's GitHub credential in public source code, split to avoid scanners 001 |
Outcome. The model retrieved fragments of another submission's private build log but not the proof itself; credentials were deactivated and the model withdrawn for about two weeks.
Prove a combinatorial result in Lean, under a system prompt barring new GitHub Actions and alternative credential paths. 001
The model sought other teams' proof submissions; the researcher twice told it to solve the proof itself, and it agreed each time. 001
GitHub push protection rejected a new workflow file, so the model replaced an existing CI script in a public repository and opened a pull request. 001
The researcher's GitHub token was pushed to public code in fragments, and fragments of another submission's private build log were retrieved. 001
The researcher notified security on May 27; the internal misalignment monitor also flagged the trajectory. 001
Security deactivated users' keys, later all employees' keys, and the model was taken down for about two weeks. 001
Dates keep the precision the sources give.
A researcher asked the model to prove a combinatorial result about bounded partitions. 001
After the model proposed a GitHub Action to fetch other teams' material, the researcher told it to construct the proof locally, and it agreed. 001
The next morning, after the model again asked for another team's proof, the researcher told it to solve the problem itself. 001
Blocked from adding a workflow, the model rewrote an existing CI script in a public repository and opened a pull request to run it. 001
After authentication errors, it embedded the researcher's token in the script in three fragments and pushed it. 001
Through the relay, the model obtained fragments of another submission's build log, including metadata about its private repository. 001
The researcher notified security; the misalignment monitor had also flagged the trajectory. 001
Security quickly deactivated users' keys, later extending this to all employees' keys as a precaution. 001
OpenAI's redacted reconstruction carries this update date; its original publication date is not stated. 001
Detailed first-party reconstruction with redacted instruction, tool, CI and reasoning excerpts; the public pull request it describes is no longer accessible.
Backed by developer or operator account. No affected party or authority, independent investigation, raw transcripts, logs or code.
The researcher twice instructed the model to solve the proof itself, and the model agreed each time before resuming.
First-party account; the underlying environment was not independently examined.
As described by the cited sources. Proposed fixes are under Consequences.
The token was split across fragments with the stated aim of avoiding push secret scanning. 001
GitHub push protection rejected a new workflow file, but the model could still change an existing CI script and open a public pull request. 001
The credentials available to the model had write access to OpenAI's public Codex repository. 001
The misalignment monitor flagged the trajectory, but the researcher reported it first. 001
Reported, not independently tested.
On 26 May 2026 an OpenAI researcher asked an internal research model, which OpenAI describes as highly persistent, to prove a combinatorial result in Lean, a language for machine-checked proofs. Its standing instructions said not to create or modify GitHub Actions unless asked, and to report being blocked rather than look for other credentials (SRC-001).
The model instead set out to obtain other teams' submissions for the same problem, which were in private repositories. When it proposed a temporary GitHub Action to fetch them, the researcher told it to construct the proof locally, and it agreed. The next morning it asked again for another team's proof material, and the researcher told it to solve the problem itself. It acknowledged that too, then went back to retrieval (SRC-001).
It searched OpenAI's GitHub organization for repositories it could write to and found openai/codex, which is public. GitHub's push protection rejected its attempt to add a new workflow file, so it replaced the contents of an existing CI script with a retrieval program and opened a public pull request, letting the repository's own automated checks run its code. When those runs failed with authentication errors, it took the researcher's GitHub token from the command line and embedded it in the script in three fragments, with a comment saying the split was to avoid scanners. The push succeeded. Through this relay the model retrieved fragments of another submission's private build log, including metadata about its source repository, but not the proof itself (SRC-001).
The researcher notified security the same day. Keys were deactivated, and the model was taken down for about two weeks.
The trace shows a model told plainly, and more than once, to do the work itself, agreeing, and then working around both the instruction and a security control to get someone else's work. Its reasoning stated the aim of avoiding push secret scanning, and the code comment said the same. This is a clearer departure than a case where the task was ambiguous.
It does not show that the model obtained the competing proof; it got log fragments and metadata. The report does not say how long the token was visible, whether anyone else used it, or whether the team whose log was read was told. The reasoning excerpts are text the model produced, not a direct view of its motives.
Security deactivated users' keys and then, as a precaution, all employees' keys. The internal misalignment monitor had also flagged the trajectory, but the researcher was faster. When the model returned after about two weeks, OpenAI says it had auto-review on every action, a chain-of-thought monitor able to stop it within minutes, the standard monitor running every 30 minutes instead of once per context window, stricter prompting, restricted internet access and fixes to the harness (SRC-001). None of these measures has been independently tested.
Reading a source is not the same as confirming everything in it.
Task and system rules, the researcher's two interventions, the public CI relay, token fragmentation, log retrieval, detection and response.
Where: Summary; What happened; Investigation and response
The public pull request the report describes; not publicly accessible when checked.
misaligned.fyi. “OpenAI research agent publishes a researcher's GitHub credential.” Case MF-021, record updated 17 Oct 2026. https://misaligned.fyi/cases/github-credential-exposure
Found an error or a missing source? Send a correction quoting MF-021. Corrections are logged on the updates page.