Chat logs
Show the chat that found the proof
A proof settles the statement. The chat behind it shows how a model got there, wrong turns included. Proofs of new problems now come with their chat, and proofs accepted before can send theirs for a bonus.
Bonus for earlier proofs
- Erdős problem
- $500
- Any other problem
- $250
Paid in Subnet 66 alpha worth that amount on the day it is paid. Your original reward does not change.
For proofs submitted before 13 Oct 2026. Claim by 13 Oct 2027.
Inside a package
Every step of the session, filed
The agent copies the session event by event and keeps what each step produced. The proof's hash closes the package, so it belongs to one proof and no other.
Session
- user
Prove the statement in Main.lean. Keep every failed attempt.
- assistant
Induction on n, with the bound from the second lemma for the step.
- tool
$ lake build
error: unsolved goals ⊢ n + 1 ≤ 2 ^ n
- assistant
The base case needs n ≥ 1. Strengthening the hypothesis and building again.
- tool
$ lake build
Build completed successfully.
- tool
$ sha256sum Main.lean
9f3c41d0…a71e
Package
- events.jsonl6 events
- artifacts/
- build-1.log
- build-2.log
- Main.lean
- manifest.jsonfinal_proof_sha256 9f3c41d0…a71e
Ready to upload. The hash matches the proof you submit.
Two ways in
When the logs are due
New problems: logs go in with the proof
On the submit page, upload the logs first, then submit the proof within 24 hours. A proof without its logs is not accepted, and no credit is spent. The logs cannot be added or replaced afterwards.
The bounty is paid only if the logs are accepted. If they are rejected or withdrawn, the proof earns no bounty and the problem reopens to other solvers.
Earlier proofs: a bonus for the logs
If you own a proof submitted before intake opened that was approved for its full bounty, open it under your submissions and upload its chat logs there.
The chat must show the proof before the date you submitted it.
Preparing the file
Your agent builds the package
Found the proof with Claude Code or Codex? Your sessions are already saved on your computer, so there is nothing to export.
Copy the message
The submit page, or the proof's page under your submissions, shows a message with your proof's details filled in.
Give it to your agent
Open Claude Code or Codex on the computer where you worked, paste the message and add the path to your proof file.
Upload the zip
The agent finds the session, writes chat-log-package.zip and tells you what is in it and what is missing. Upload that file on the same page.
Worked in ChatGPT or Claude on the web? Export your data first (in ChatGPT: Settings, Data controls, Export data; in Claude: Settings, Privacy, Export data), then give the export to Claude Code or Codex with the same message.
What we check
The original chat, not a retelling
That these are the chat logs that produced the proof, not a recreation of them.
- As it happened
- Messages are copied as they were. Nothing is rewritten, and hidden model reasoning is left out.
- Failures kept
- Failed attempts and tool output stay in. They are part of how the proof was found.
- Secrets removed
- The agent strips passwords and keys before packing. One zip, at most 64 MiB.