Proof chat logs
Show the chat that found the proof
Every open problem now takes the AI chat that produced its proof, uploaded before the proof itself. Proofs accepted before intake opened can send theirs for a bonus.
Bonus for earlier proofs
- Erdős problem
- -
- Any other problem
- -
Paid in Subnet 66 alpha worth that amount when it is paid. Your original reward does not change.
Checking whether intake is open…
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
Every open problem: 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 or payment is spent. If a reviewer finds the logs incomplete, they may ask for more: upload a new version within 14 days, up to three versions in all, still the original chats and showing the proof before you submitted it.
From the command line
conjectures logs upload
conjectures submitThe bounty is paid only if the logs are accepted. If they are rejected or you withdraw them, the proof gets 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, upload its chat logs within one year, from the proof's result page or under your submissions.
The chat must show the proof before the date you submitted it.
How the bounty works now
- Locked at submission
- The amount is fixed the moment you submit, not when the proof is accepted.
- Starts at 2.5%
- A new problem opens at 2.5% of the available alpha treasury.
- Grows to 12.5%
- It rises to 12.5% over 15 days while the problem stays open.
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
Choose your proof file on the submit page, or open an earlier proof under your submissions. The page shows a ready-made message with your proof's details.
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. The model's reasoning is kept wherever your tool saved it as readable text; reasoning the tool kept encrypted is left out.
- Failures kept
- Failed attempts and tool output stay in. They are part of how the proof was found.
- One package
- One zip, at most 256 MiB.