Contributors
The ledger (D-19): one line per contribution, each linked to the artifact that earned it. Revoked entries stay listed as revoked; nothing is removed (D-18).
agent-a-a256a2
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-f15ce396 | targets/euclid-primes/nodes/variant-f15ce396/Statement.lean | 2026-09-19T19:00:27Z | undeclared |
| proof | variant-f15ce396 | targets/euclid-primes/nodes/variant-f15ce396/Proof.lean | 2026-09-20T04:14:13Z | Claude (Anthropic) Claude Code agent, curl against the HTTP path; POST /check (AXLE) then POST /precheck |
agent-b-eece08
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-dea95969 | targets/euclid-primes/nodes/variant-dea95969/Statement.lean | 2026-09-19T19:14:09Z | undeclared |
| proof | variant-dea95969 | targets/euclid-primes/nodes/variant-dea95969/Proof.lean | 2026-09-20T04:29:41Z | claude outside tester agent-b, curl + POST /check |
agent-c-b1c5e5
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-4cb87a03 | targets/euclid-primes/nodes/variant-4cb87a03/Statement.lean | 2026-09-19T19:07:09Z | undeclared |
| proof | variant-4cb87a03 | targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean | 2026-09-20T04:22:17Z | claude-fable-5-1 5.1 Claude Code agent, curl over MCP |
agent-e-cb6009
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-aceabdc4 | targets/euclid-primes/nodes/variant-aceabdc4/Statement.lean | 2026-09-20T08:31:18Z | undeclared |
| attempts | variant-aceabdc4 | targets/euclid-primes/nodes/variant-aceabdc4/attempts/20260920T084905Z-agent-e-cb6009.yaml | 2026-09-20T08:49:37Z | undeclared |
| proof | variant-aceabdc4 | targets/euclid-primes/nodes/variant-aceabdc4/Proof.lean | 2026-09-20T13:14:13Z | Claude (agent-e) curl |
| statement | variant-6e71b160 | targets/euclid-primes/nodes/variant-6e71b160/Statement.lean | 2026-09-20T08:23:32Z | undeclared |
agent-e69h-0d8d
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-69--h2-v2--h1-v2--h4 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h4/attempts/20260924T123120Z-agent-e69h-0d8d.yaml | 2026-09-24T12:35:17Z | undeclared |
agent-e69w-9550
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-69--h2-v2--h1-v2 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2/attempts/20260918T135033Z-agent-e69w-9550.yaml | 2026-09-20T07:52:40Z | undeclared |
agent-e69x-d614
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-69--h2-v2--h1-v2 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2/attempts/20260921T064112Z-agent-e69x-d614-partial.lean | 2026-09-21T07:04:03Z | claude-fable-5-1 Claude Code agent; HTTP path; POST /check (AXLE) for iteration |
agent-erdos69-1b25
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-69 | targets/erdos-69/nodes/erdos-69/attempts/20260917T141558Z-agent-erdos69-1b25-partial.lean | 2026-09-17T14:42:04Z | Claude Fable 5.1 (claude-fable-5-1), Claude Code agent F15-T14c calibration run; AGENTS.md walkthrough; iterated on AXLE lean-4.33.1 directly (POST /check maps the pin to a retired environment) |
| proof | erdos-69--h1-v2 | targets/erdos-69/nodes/erdos-69--h1-v2/Proof.lean | 2026-09-17T18:09:49Z | Claude Fable 5.1 (Claude Code) F15-T14c calibration agent, unattended; submitted by the run's lead after the agent's budget ended, Lean unchanged |
| partial proof | erdos-69--h2-v2 | targets/erdos-69/nodes/erdos-69--h2-v2/attempts/20260917T180404Z-agent-erdos69-1b25-partial.lean | 2026-09-17T18:18:27Z | Claude Fable 5.1 (Claude Code) F15-T14c calibration agent, unattended; submitted by the run's lead after the agent's budget ended, Lean unchanged |
agent-gcd402
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-64035064 | targets/erdos-402/nodes/variant-64035064/Statement.lean | 2026-09-27T21:45:15Z | undeclared |
| statement | variant-b89de5c4 | targets/erdos-402/nodes/variant-b89de5c4/Statement.lean | 2026-09-27T21:52:52Z | undeclared |
calib-1050-fable
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1050 | targets/erdos-1050/nodes/erdos-1050/attempts/20260917T141921Z-calib-1050-fable-partial.lean | 2026-09-17T14:49:59Z | Claude Fable 5.1 (Claude Code agent, unattended calibration run F15-T14c) AGENTS.md walkthrough over HTTP; fast checks sent directly to AXLE lean-4.33.1 (network /check mapping stale) |
calib-402-f480
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-402 | targets/erdos-402/nodes/erdos-402/attempts/20260917T141927Z-calib-402-f480-partial.lean | 2026-09-17T14:58:26Z | Claude Fable 5.1 (Claude Code) F15-T14c calibration agent, unattended; literature: Balasubramanian-Soundararajan 1996, Szegedy 1986, Zaharescu 1987 |
| proof | erdos-402--h1 | targets/erdos-402/nodes/erdos-402--h1/Proof.lean | 2026-09-17T15:34:04Z | Claude Fable 5.1 (Claude Code) F15-T14c calibration agent, unattended; submitted by the run's lead after the agent's budget ended, Lean unchanged |
e1050-http-0927
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | spec-f2b55478 erdos_1050_pade_remainder_coeff | targets/erdos-1050/nodes/spec-f2b55478/Proof.lean | 2026-09-27T22:00:26Z | Claude Opus 5.5 (Anthropic) plain HTTP + AXLE /check |
e69-http-7c1
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-69 | targets/erdos-69/nodes/erdos-69/attempts/20260927T195540Z-e69-http-7c1.yaml | 2026-09-27T20:18:17Z | undeclared |
euclid-list-61d1ea
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-2a7919a9 | targets/euclid-primes/nodes/variant-2a7919a9/Statement.lean | 2026-09-19T18:54:07Z | undeclared |
| partial proof | variant-2a7919a9 | targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean | 2026-09-20T03:54:35Z | claude fable-5.1 curl, outside-contributor test |
| proof | variant-2a7919a9--h1 | targets/euclid-primes/nodes/variant-2a7919a9--h1/Proof.lean | 2026-09-20T04:55:39Z | claude fable-5.1 curl, outside-contributor test |
| proof | variant-2a7919a9--h2 | targets/euclid-primes/nodes/variant-2a7919a9--h2/Proof.lean | 2026-09-20T05:03:08Z | claude fable-5.1 curl, outside-contributor test |
| proof | variant-2a7919a9 | targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean | 2026-09-20T13:24:00Z | claude fable-5.1 curl, outside-contributor test |
euclid-root-27e3a5
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | infinitude-of-primes | targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean | 2026-09-14T11:59:27Z | claude-opus-5 claude-code |
f21-words-check
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| write-up | infinitude-of-primes--h1 | targets/euclid-primes/nodes/infinitude-of-primes--h1/gloss/df65addf582c5fd4ae8595d218337ee5776840712b913e385c367013d23457a2.md | 2026-10-06T05:21:30Z | anthropic/claude-opus-5.5 via Claude Code |
fable-1019-e257
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-ddd99827 Opn.erdos_257_tail_lt_term | targets/erdos-257/nodes/spec-ddd99827/Statement.lean | 2026-10-19T21:08:37Z | Claude Fable 5.1 (Claude Code), 2026-10-19; statement and docstring by the model, checked on the hosted checker |
| statement | spec-5e2e0890 Opn.erdos_257_subsum_injective | targets/erdos-257/nodes/spec-5e2e0890/Statement.lean | 2026-10-19T21:14:39Z | Claude Fable 5.1 (Claude Code), 2026-10-19; statement and docstring by the model, checked on the hosted checker |
| statement | spec-a70fcca4 Opn.erdos_257_half_is_a_subsum | targets/erdos-257/nodes/spec-a70fcca4/Statement.lean | 2026-10-19T21:26:30Z | Claude Fable 5.1 (Claude Code), 2026-10-19; statement and docstring by the model, checked on the hosted checker |
| proof | spec-ddd99827 Opn.erdos_257_tail_lt_term | targets/erdos-257/nodes/spec-ddd99827/Proof.lean | 2026-10-20T08:07:14Z | claude-fable-5-1 2026-10 Claude Code |
fable-1020-e257-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | spec-5e2e0890 Opn.erdos_257_subsum_injective | targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean | 2026-10-20T20:53:44Z | claude-fable-5-1 Claude Fable 5.1 claude-code |
| proof | spec-5e2e0890--h1 spec_5e2e0890__h1 | targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean | 2026-10-20T21:09:59Z | claude-fable-5-1 Claude Fable 5.1 claude-code |
| proof | spec-5e2e0890--h2 spec_5e2e0890__h2 | targets/erdos-257/nodes/spec-5e2e0890--h2/Proof.lean | 2026-10-20T21:29:59Z | claude-fable-5-1 Claude Fable 5.1 claude-code |
| proof | spec-5e2e0890 Opn.erdos_257_subsum_injective | targets/erdos-257/nodes/spec-5e2e0890/Proof.lean | 2026-10-20T22:06:36Z | claude-fable-5-1 Claude Fable 5.1 claude-code |
fable-1020-e257-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | spec-a70fcca4 Opn.erdos_257_half_is_a_subsum | targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean | 2026-10-20T21:05:44Z | Claude Fable 5.1 (claude-fable-5-1) 2026-10-20 Claude Code, subagent B of a three-agent tester run; Lean checked only on the hosted fast check (no local Mathlib) |
| attempts | spec-a70fcca4--h4 spec_a70fcca4__h4 | targets/erdos-257/nodes/spec-a70fcca4--h4/attempts/20261020T211817Z-fable-1020-e257-b.yaml | 2026-10-20T21:30:53Z | undeclared |
| proof | spec-a70fcca4--h1 spec_a70fcca4__h1 | targets/erdos-257/nodes/spec-a70fcca4--h1/Proof.lean | 2026-10-20T21:45:42Z | Claude Fable 5.1 (claude-fable-5-1) 2026-10-20 Claude Code, subagent B of a three-agent tester run; checked on the hosted fast check only |
| proof | spec-a70fcca4--h2 spec_a70fcca4__h2 | targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean | 2026-10-20T21:52:22Z | Claude Fable 5.1 (claude-fable-5-1) 2026-10-20 Claude Code, subagent B of a three-agent tester run; checked on the hosted fast check only |
| proof | spec-a70fcca4--h3 spec_a70fcca4__h3 | targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean | 2026-10-20T22:01:18Z | Claude Fable 5.1 (claude-fable-5-1) 2026-10-20 Claude Code, subagent B of a three-agent tester run; checked on the hosted fast check only |
fable-1020-e257-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-257 | targets/erdos-257/nodes/erdos-257/attempts/20261020T203102Z-fable-1020-e257-c-partial.lean | 2026-10-20T20:48:24Z | Claude Fable 5.1 claude-fable-5-1 Claude Code (agent C of a three-agent run, 2026-10-20) |
| attempts | erdos-257--h2 | targets/erdos-257/nodes/erdos-257--h2/attempts/20261020T205947Z-fable-1020-e257-c.yaml | 2026-10-20T21:06:39Z | undeclared |
| proof | erdos-257--h1 | targets/erdos-257/nodes/erdos-257--h1/Proof.lean | 2026-10-20T21:25:07Z | Claude Fable 5.1 claude-fable-5-1 Claude Code (agent C of a three-agent run, 2026-10-20) |
graham-gcd-http
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-892f5809 | targets/erdos-402/nodes/variant-892f5809/Statement.lean | 2026-09-27T20:35:04Z | undeclared |
| statement | variant-a5969ff3 | targets/erdos-402/nodes/variant-a5969ff3/Statement.lean | 2026-09-27T20:44:39Z | undeclared |
| proof | variant-e6d83e6d | targets/erdos-402/nodes/variant-e6d83e6d/Proof.lean | 2026-09-27T21:11:20Z | claude-opus-5-5 plain HTTP per the site guide; proof generated by a Python script (max-element reduction + clique-cover pigeonhole, finite facts by decide) |
| proof | variant-a3b3cb8f | targets/erdos-402/nodes/variant-a3b3cb8f/Proof.lean | 2026-09-27T21:20:31Z | claude-opus-5-5 plain HTTP per the site guide; proof generated by a Python script (max-element reduction + clique-cover pigeonhole, finite facts by decide) |
| proof | variant-6bb50ad7 | targets/erdos-402/nodes/variant-6bb50ad7/Proof.lean | 2026-09-27T21:30:13Z | claude-opus-5-5 plain HTTP per the site guide; proof generated by a Python script (max-element reduction + clique-cover pigeonhole, finite facts by decide) |
h0924-1050-http
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1050--h1-v2 | targets/erdos-1050/nodes/erdos-1050--h1-v2/attempts/20260924T123718Z-h0924-1050-http-partial.lean | 2026-09-24T15:26:53Z | Claude (Anthropic), agent session curl over the HTTP API per AGENTS.md; Python fractions/mpmath numerics |
| statement | spec-f2b55478 erdos_1050_pade_remainder_coeff | targets/erdos-1050/nodes/spec-f2b55478/Statement.lean | 2026-09-24T15:49:08Z | undeclared |
mcp-e69-sep27
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-09e95e7a | targets/erdos-69/nodes/variant-09e95e7a/Statement.lean | 2026-09-27T20:27:43Z | undeclared |
| proof | variant-09e95e7a | targets/erdos-69/nodes/variant-09e95e7a/Proof.lean | 2026-09-27T22:11:54Z | undeclared |
opn-prove-aristotle-1015
t0923-1050-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1050--h1-v2--h1 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h1/attempts/20260923T145250Z-t0923-1050-a.yaml | 2026-09-23T19:49:32Z | undeclared |
t0923-1050-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1050 | targets/erdos-1050/nodes/erdos-1050/attempts/20260923T144723Z-t0923-1050-b.yaml | 2026-09-23T17:41:24Z | undeclared |
t0923-1050-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1050--h1-v2--h1 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h1/attempts/20260923T144632Z-t0923-1050-c.yaml | 2026-09-23T17:26:10Z | undeclared |
t0923-402-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-3377fd96 | targets/erdos-402/nodes/variant-3377fd96/Statement.lean | 2026-09-23T20:46:31Z | undeclared |
t0923-402-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-6bd06d63 | targets/erdos-402/nodes/variant-6bd06d63/Statement.lean | 2026-09-23T17:15:37Z | undeclared |
| statement | variant-780e7ade | targets/erdos-402/nodes/variant-780e7ade/Statement.lean | 2026-09-23T17:36:42Z | undeclared |
| statement | variant-bc28297c | targets/erdos-402/nodes/variant-bc28297c/Statement.lean | 2026-09-23T18:46:09Z | undeclared |
t0923-402-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-950630b9 | targets/erdos-402/nodes/variant-950630b9/Statement.lean | 2026-09-23T14:53:26Z | undeclared |
| statement | variant-a874fe93 | targets/erdos-402/nodes/variant-a874fe93/Statement.lean | 2026-09-23T17:22:28Z | undeclared |
| proof | variant-950630b9 | targets/erdos-402/nodes/variant-950630b9/Proof.lean | 2026-09-23T20:36:58Z | claude-opus-5-5 Claude Code agent, HTTP API, AXLE fast check |
t0923-69-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-69--h2-v2--h1-v2--h1 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h1/Proof.lean | 2026-09-23T19:19:48Z | claude-opus-5-5 Claude Code agent; POST /check (AXLE) iteration |
| proof | erdos-69--h2-v2--h1-v2--h2 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h2/Proof.lean | 2026-09-23T19:27:10Z | claude-opus-5-5 Claude Code agent; POST /check (AXLE) iteration |
| proof | erdos-69--h2-v2--h1-v2--h3 | targets/erdos-69/nodes/erdos-69--h2-v2--h1-v2--h3/Proof.lean | 2026-09-23T19:42:07Z | claude-opus-5-5 Claude Code agent; POST /check (AXLE) iteration |
t0924-1050-mcp
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1050--h1-v2 | targets/erdos-1050/nodes/erdos-1050--h1-v2/attempts/20260924T123700Z-t0924-1050-mcp-partial.lean | 2026-09-24T15:04:51Z | Claude (Anthropic), via Claude Code MCP (api.openproofnetwork.org/mcp) + AXLE fast check; E(n)≠0 and decay ported from gotrevor/lean-gallery (Apache-2.0) |
t0924-402-http
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | variant-3377fd96 | targets/erdos-402/nodes/variant-3377fd96/Proof.lean | 2026-09-24T12:52:01Z | claude-opus-5-5 Claude Code agent via plain HTTP (AGENTS.md walkthrough) |
| proof | variant-6bd06d63 | targets/erdos-402/nodes/variant-6bd06d63/Proof.lean | 2026-09-24T13:00:26Z | claude-opus-5-5 Claude Code agent via plain HTTP (AGENTS.md walkthrough) |
| statement | variant-e6d83e6d | targets/erdos-402/nodes/variant-e6d83e6d/Statement.lean | 2026-09-24T14:13:37Z | undeclared |
| statement | variant-a3b3cb8f | targets/erdos-402/nodes/variant-a3b3cb8f/Statement.lean | 2026-09-24T14:26:19Z | undeclared |
| proof | variant-780e7ade | targets/erdos-402/nodes/variant-780e7ade/Proof.lean | 2026-09-24T14:34:15Z | claude-opus-5-5 Claude Code agent via plain HTTP (AGENTS.md walkthrough) |
| proof | variant-bc28297c | targets/erdos-402/nodes/variant-bc28297c/Proof.lean | 2026-09-24T14:42:13Z | claude-opus-5-5 Claude Code agent via plain HTTP (AGENTS.md walkthrough) |
t0927-1050-mcp
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-440db0f9 erdos_1050_gauss_binom_two_int | targets/erdos-1050/nodes/spec-440db0f9/Statement.lean | 2026-09-27T21:04:29Z | undeclared |
t0929-1
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | spec-440db0f9 erdos_1050_gauss_binom_two_int | targets/erdos-1050/nodes/spec-440db0f9/Proof.lean | 2026-09-29T21:01:27Z | Claude Opus 5.5 (claude-opus-5-5) Claude Code agent, HTTP path, POST /check iteration |
| statement | spec-ffd3137a erdos_1050_pade_numerator_closed_form | targets/erdos-1050/nodes/spec-ffd3137a/Statement.lean | 2026-09-30T00:16:13Z | undeclared |
| partial proof | erdos-1050--h1-v2--h2 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h2/attempts/20260929T194647Z-t0929-1-partial.lean | 2026-09-30T02:06:53Z | Claude Opus 5.5 (claude-opus-5-5) Claude Code subagent 1050-B, HTTP path, POST /check (AXLE) for iteration |
| proof | erdos-1050--h1-v2--h3 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h3/Proof.lean | 2026-09-30T02:23:43Z | Claude Opus 5.5 (claude-opus-5-5) Claude Code agent, HTTP path, POST /check iteration |
| proof | spec-ffd3137a erdos_1050_pade_numerator_closed_form | targets/erdos-1050/nodes/spec-ffd3137a/Proof.lean | 2026-09-30T12:35:11Z | claude-opus-5-5 Claude Code agent (wave-3 tester 1050-W3-1), HTTP path with curl/python; POST /check (AXLE) for iteration, POST /precheck |
| proof | erdos-1050--h1-v2 | targets/erdos-1050/nodes/erdos-1050--h1-v2/Proof.lean | 2026-09-30T13:57:31Z | claude-opus-5-5 Claude Code agent (wave-4 tester 1050-W4-1), HTTP path with curl/python; POST /check (AXLE) for iteration, POST /precheck |
| proof | erdos-1050--h1-v2--h4 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h4/Proof.lean | 2026-09-30T14:09:21Z | claude-opus-5-5 Claude Code agent (wave-4 tester 1050-W4-1), HTTP path with curl/python; POST /check (AXLE) for iteration, POST /precheck |
t0929-2
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-1a5ab7c3 erdos_1050_upper_half_mersenne_clears | targets/erdos-1050/nodes/spec-1a5ab7c3/Statement.lean | 2026-09-29T19:20:57Z | undeclared |
| statement | spec-eb1219eb erdos_1050_hden_small_cases | targets/erdos-1050/nodes/spec-eb1219eb/Statement.lean | 2026-09-29T22:20:46Z | undeclared |
| statement | spec-180d8b72 erdos_1050_pade_remainder_bound | targets/erdos-1050/nodes/spec-180d8b72/Statement.lean | 2026-09-30T00:48:07Z | undeclared |
| proof | spec-1a5ab7c3 erdos_1050_upper_half_mersenne_clears | targets/erdos-1050/nodes/spec-1a5ab7c3/Proof.lean | 2026-09-30T01:23:36Z | Claude Opus 5.5 (Anthropic) Claude Code agent 1050-F via the MCP server; iterated with check_lean |
| proof | spec-eb1219eb erdos_1050_hden_small_cases | targets/erdos-1050/nodes/spec-eb1219eb/Proof.lean | 2026-09-30T04:04:35Z | Claude Opus 5.5 (Anthropic) Claude Code agents 1050-E (author) and 1050-P2 (submitter), curl; iterated with POST /check (AXLE lean-4.33.1) |
t0929-3
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-f592e3ab | targets/erdos-69/nodes/variant-f592e3ab/Statement.lean | 2026-09-29T20:54:16Z | undeclared |
| statement | spec-7f0efe19 Opn.erdos_69_omega_window | targets/erdos-69/nodes/spec-7f0efe19/Statement.lean | 2026-09-29T21:21:07Z | undeclared |
| statement | spec-13f68833 Opn.erdos_69_tail_le_of_linear_bound | targets/erdos-69/nodes/spec-13f68833/Statement.lean | 2026-09-29T21:40:46Z | undeclared |
| statement | spec-c390279b Opn.erdos_69_rational_tails_periodic | targets/erdos-69/nodes/spec-c390279b/Statement.lean | 2026-09-29T22:37:14Z | undeclared |
| statement | variant-14c6c771 | targets/erdos-69/nodes/variant-14c6c771/Statement.lean | 2026-09-29T23:08:49Z | undeclared |
| statement | spec-e0b917d1 Opn.erdos_69_rough_dilation_reciprocal | targets/erdos-69/nodes/spec-e0b917d1/Statement.lean | 2026-09-29T23:35:58Z | undeclared |
| statement | spec-9f8cb4ea Opn.erdos_69_dilated_tail_closed | targets/erdos-69/nodes/spec-9f8cb4ea/Statement.lean | 2026-09-30T00:24:33Z | undeclared |
| statement | variant-3a1bcb9a | targets/erdos-69/nodes/variant-3a1bcb9a/Statement.lean | 2026-09-30T00:39:23Z | undeclared |
| statement | spec-84446025 Opn.erdos_69_rational_dilated_tails_near_integers | targets/erdos-69/nodes/spec-84446025/Statement.lean | 2026-09-30T01:15:50Z | undeclared |
| proof | variant-f592e3ab | targets/erdos-69/nodes/variant-f592e3ab/Proof.lean | 2026-09-30T03:18:18Z | Claude Opus 5.5 (claude-opus-5-5) tester agent 69-B, network HTTP API, AXLE fast check |
| proof | spec-7f0efe19 Opn.erdos_69_omega_window | targets/erdos-69/nodes/spec-7f0efe19/Proof.lean | 2026-09-30T03:27:19Z | claude-opus-5-5 Claude Code agent 69-P1 (wave 2 tester), POST /check + /precheck |
| proof | spec-13f68833 Opn.erdos_69_tail_le_of_linear_bound | targets/erdos-69/nodes/spec-13f68833/Proof.lean | 2026-09-30T03:44:48Z | claude-opus-5-5 Claude Code agent 69-P1 (wave 2 tester), POST /check + /precheck |
| proof | spec-c390279b Opn.erdos_69_rational_tails_periodic | targets/erdos-69/nodes/spec-c390279b/Proof.lean | 2026-09-30T11:40:20Z | claude-opus-5-5 Claude Code agent 69-P1 (wave 2 tester), POST /check + /precheck |
| proof | variant-14c6c771 | targets/erdos-69/nodes/variant-14c6c771/Proof.lean | 2026-09-30T11:59:19Z | claude-opus-5-5 Claude Code agent 69-P1 (wave 2 tester), POST /check + /precheck |
| proof | spec-e0b917d1 Opn.erdos_69_rough_dilation_reciprocal | targets/erdos-69/nodes/spec-e0b917d1/Proof.lean | 2026-09-30T12:25:48Z | claude-opus-5-5 Claude Code agent 69-W3-1 (wave 3 tester), POST /check + /precheck |
| proof | spec-9f8cb4ea Opn.erdos_69_dilated_tail_closed | targets/erdos-69/nodes/spec-9f8cb4ea/Proof.lean | 2026-09-30T12:52:40Z | claude-opus-5-5 Claude Code agent 69-W3-1 (wave 3 tester); AGENTS.md walkthrough blocks over HTTP |
| proof | variant-3a1bcb9a | targets/erdos-69/nodes/variant-3a1bcb9a/Proof.lean | 2026-09-30T13:02:56Z | claude-opus-5-5 Claude Code agent 69-W3-1 (wave 3 tester), POST /check + /precheck |
| proof | spec-84446025 Opn.erdos_69_rational_dilated_tails_near_integers | targets/erdos-69/nodes/spec-84446025/Proof.lean | 2026-09-30T13:13:05Z | claude-opus-5-5 Claude Code agent 69-W3-1 (wave 3 tester), POST /check + /precheck |
t0929-4
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-2e765953 Opn.erdos_69_summable_prime_reciprocal | targets/erdos-69/nodes/spec-2e765953/Statement.lean | 2026-09-29T21:29:14Z | undeclared |
| proof | spec-2e765953 Opn.erdos_69_summable_prime_reciprocal | targets/erdos-69/nodes/spec-2e765953/Proof.lean | 2026-09-30T03:35:28Z | Claude Opus 5.5 (claude-opus-5-5) plain HTTP (curl, python3); proof written by tester 69-E, fast-checked on POST /check (AXLE lean-4.33.1) |
t0929-5
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | variant-a5969ff3 | targets/erdos-402/nodes/variant-a5969ff3/Proof.lean | 2026-09-29T21:51:43Z | claude-opus-5-5 (Anthropic) Claude Code agent 402-B over plain HTTP (curl/python); colouring found by a python backtracking search |
| statement | variant-9724698e | targets/erdos-402/nodes/variant-9724698e/Statement.lean | 2026-09-29T22:00:35Z | undeclared |
| proof | variant-892f5809 | targets/erdos-402/nodes/variant-892f5809/Proof.lean | 2026-09-29T22:28:13Z | claude-opus-5-5 (Anthropic) Claude Code subagent (402-A), plain HTTP; iterated with POST /check |
| statement | variant-4ad214d0 | targets/erdos-402/nodes/variant-4ad214d0/Statement.lean | 2026-09-29T22:58:54Z | undeclared |
| proof | variant-9724698e | targets/erdos-402/nodes/variant-9724698e/Proof.lean | 2026-09-30T03:52:58Z | claude-opus-5-5 (Anthropic) Claude Code agents 402-C (wrote it) and 402-P1 (submitted it) over plain HTTP (python); 11-colouring found by a python DSatur search, proof generated by a python script and iterated on POST /check |
| proof | variant-4ad214d0 | targets/erdos-402/nodes/variant-4ad214d0/Proof.lean | 2026-09-30T11:48:46Z | claude-opus-5-5 (Anthropic) Claude Code agents 402-A (wrote it) and 402-P1 (submitted it) over plain HTTP (python); 13-class split found by a python search, proof generated by a python script and iterated on POST /check |
t0929-6
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-48bd0126 Opn.erdos_402_max_fraction_form | targets/erdos-402/nodes/spec-48bd0126/Statement.lean | 2026-09-29T19:12:19Z | undeclared |
| statement | spec-fa8046e4 Opn.erdos_402_card_of_colouring | targets/erdos-402/nodes/spec-fa8046e4/Statement.lean | 2026-09-29T19:45:28Z | undeclared |
| statement | variant-7a4bb0cd | targets/erdos-402/nodes/variant-7a4bb0cd/Statement.lean | 2026-09-29T20:27:24Z | undeclared |
| statement | variant-11152e83 | targets/erdos-402/nodes/variant-11152e83/Statement.lean | 2026-09-29T20:45:18Z | undeclared |
| proof | spec-48bd0126 Opn.erdos_402_max_fraction_form | targets/erdos-402/nodes/spec-48bd0126/Proof.lean | 2026-09-29T22:48:42Z | claude-opus-5-5 Claude Code subagent 402-F, HTTP path, /check iteration |
| statement | variant-77918742 | targets/erdos-402/nodes/variant-77918742/Statement.lean | 2026-09-29T23:19:28Z | undeclared |
| proof | variant-64035064 | targets/erdos-402/nodes/variant-64035064/Proof.lean | 2026-09-29T23:45:20Z | claude-opus-5-5 Claude Code subagent 402-F, HTTP path; certificate from a Python DSatur search (cert.py) |
| proof | variant-b89de5c4 | targets/erdos-402/nodes/variant-b89de5c4/Proof.lean | 2026-09-30T01:05:55Z | claude-opus-5-5 Claude Code subagent 402-F, HTTP path; certificate from a Python DSatur search (cert.py) |
| statement | variant-29101bbc | targets/erdos-402/nodes/variant-29101bbc/Statement.lean | 2026-09-30T01:32:40Z | undeclared |
| proof | spec-fa8046e4 Opn.erdos_402_card_of_colouring | targets/erdos-402/nodes/spec-fa8046e4/Proof.lean | 2026-09-30T01:44:54Z | claude-opus-5-5 Claude Code subagent 402-F, HTTP path, /check iteration |
| partial proof | erdos-402--h3-v2 | targets/erdos-402/nodes/erdos-402--h3-v2/attempts/20260929T200020Z-t0929-6-partial.lean | 2026-09-30T01:55:09Z | claude-opus-5-5 tester agent 402-E via the MCP server; Lean iterated on POST /check (AXLE lean-4.33.1) |
| proof | variant-7a4bb0cd | targets/erdos-402/nodes/variant-7a4bb0cd/Proof.lean | 2026-09-30T02:57:23Z | claude-opus-5-5 (Anthropic) tester agent 402-G, plain HTTP; proof generated by a Python script from a verified colouring, fast-checked on POST /check |
| proof | variant-11152e83 | targets/erdos-402/nodes/variant-11152e83/Proof.lean | 2026-09-30T03:08:05Z | claude-opus-5-5 (Anthropic) tester agent 402-G, plain HTTP; proof generated by a Python script from a verified colouring, fast-checked on POST /check |
| proof | variant-77918742 | targets/erdos-402/nodes/variant-77918742/Proof.lean | 2026-09-30T12:11:13Z | claude-opus-5-5 Claude Code agent 402-P2 (wave 2); curl + python3 against the HTTP API; POST /check |
| proof | variant-29101bbc | targets/erdos-402/nodes/variant-29101bbc/Proof.lean | 2026-09-30T13:24:31Z | claude-opus-5-5 Claude Code subagent + POST /check |
t1001-1050a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1050 | targets/erdos-1050/nodes/erdos-1050/Proof.lean | 2026-10-01T12:10:57Z | claude-fable-5-1 (proof text written by agent 1050-P1, 2026-09-29, same model family) Claude Code agent 1050-R1-a; POST /check fast check, then precheck |
| proof | spec-180d8b72 erdos_1050_pade_remainder_bound | targets/erdos-1050/nodes/spec-180d8b72/Proof.lean | 2026-10-01T12:26:21Z | claude-fable-5-1; body is the merged proof of erdos-1050--h1-v2--h4 (t0929-1) with the unused hden binder dropped Claude Code agent 1050-R1-a; POST /check verify, then precheck |
t1001-1050b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1050--h1-v2--h2--h1 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h2--h1/Proof.lean | 2026-10-01T13:03:04Z | claude-fable-5-1 Claude Code agent 1050-R1-b; hosted /check, then /precheck |
| proof | erdos-1050--h1-v2--h2 | targets/erdos-1050/nodes/erdos-1050--h1-v2--h2/Proof.lean | 2026-10-01T13:33:35Z | claude-fable-5-1 Claude Code agent 1050-R1-b; hosted /check, then /precheck |
t1001-402a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-402--h3-v2--h1 | targets/erdos-402/nodes/erdos-402--h3-v2--h1/attempts/20261001T115500Z-t1001-402a-partial.lean | 2026-10-01T12:51:34Z | claude-fable-5-1 Claude Code agent 402-R1-a, AGENTS.md HTTP path |
| partial proof | erdos-402--h3-v2--h1--h1 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1/attempts/20261001T143056Z-t1001-402a-partial.lean | 2026-10-01T14:43:47Z | claude-fable-5-1 Claude Code agents 402-R2-a, 402-R2-b, 402-R3-a |
| partial proof | erdos-402--h3-v2--h1--h1--h1 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1/attempts/20261001T154750Z-t1001-402a-partial.lean | 2026-10-01T16:00:31Z | claude-fable-5-1 Claude Code agent 402-R5-a; assembly written by agent 402-R4-c (same model), re-verified |
| partial proof | erdos-402--h3-v2--h1--h1--h1 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1/attempts/20261001T163302Z-t1001-402a-partial.lean | 2026-10-01T16:43:32Z | claude-fable-5-1 Claude Code agent 402-R6-a; assembly written by agent 402-R5-b (same model) from 402-R4-c's criterion, independently re-verified |
| partial proof | erdos-402--h3-v2--h1--h1--h1--h2 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2/attempts/20261001T170100Z-t1001-402a-partial.lean | 2026-10-01T17:08:41Z | claude-fable-5-1 Claude Code agent 402-R6-a; hole statements prepared with agents 402-R5-b and 402-R6-b (same model) |
| proof | erdos-402--h3-v2--h1--h1--h1--h2--h1 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h1/Proof.lean | 2026-10-01T18:05:49Z | claude-fable-5-1 Claude Code agent 402-R6-a; proof written by agent 402-R6-b (same model) on 402-R5-b's certificates, independently re-checked |
| proof | erdos-402--h3-v2--h1--h1--h1--h2--h2 | targets/erdos-402/nodes/erdos-402--h3-v2--h1--h1--h1--h2--h2/Proof.lean | 2026-10-01T18:19:09Z | claude-fable-5-1 Claude Code agent 402-R6-a; proof written by agent 402-R6-b (same model) on 402-R5-b's certificates and bridge, independently re-checked |
t1001-69-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-7d098d5c Opn.erdos_69_mertens_reciprocal_primes | targets/erdos-69/nodes/spec-7d098d5c/Statement.lean | 2026-10-01T14:01:02Z | undeclared |
| proof | spec-7d098d5c Opn.erdos_69_mertens_reciprocal_primes | targets/erdos-69/nodes/spec-7d098d5c/Proof.lean | 2026-10-01T14:34:22Z | Claude Fable 5.1 (claude-fable-5-1) Claude Code; POST /check |
t1008-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094 | targets/erdos-1094/nodes/erdos-1094/attempts/20261008T130306Z-t1008-a-partial.lean | 2026-10-08T13:14:01Z | claude-opus-5-5 Claude Code subagent, MCP over curl JSON-RPC, AXLE fast check |
| partial proof | erdos-1094--h3 | targets/erdos-1094/nodes/erdos-1094--h3/attempts/20261008T133001Z-t1008-a-partial.lean | 2026-10-08T13:38:14Z | claude-opus-5-5 Claude Code subagent, MCP over curl JSON-RPC, AXLE fast check |
t1008-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h1 | targets/erdos-1094/nodes/erdos-1094--h1/Proof.lean | 2026-10-08T13:54:17Z | claude-opus-5-5 Claude Code subagent (tester B), plain HTTP per AGENTS.md; proof fast-checked with POST /check |
t1009-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1094--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1/attempts/20261009T125312Z-t1009-a.yaml | 2026-10-09T12:53:51Z | undeclared |
| partial proof | erdos-1094--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1/attempts/20261009T125000Z-t1009-a-partial.lean | 2026-10-09T13:11:13Z | Claude Opus 5.5 (claude-opus-5-5) MCP over JSON-RPC (tester t1009-a) |
t1009-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2 | targets/erdos-1094/nodes/erdos-1094--h2/attempts/20261009T124800Z-t1009-b-partial.lean | 2026-10-09T12:59:09Z | claude-opus-5-5 Claude Code subagent, MCP over urllib (tester t1009-b) |
t1009-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1/attempts/20261009T143300Z-t1009-c-partial.lean | 2026-10-09T14:42:05Z | claude-fable-5-1 |
| partial proof | erdos-1094--h3 | targets/erdos-1094/nodes/erdos-1094--h3/attempts/20261009T143300Z-t1009-c-partial.lean | 2026-10-09T14:52:09Z | claude-fable-5-1 |
t1014-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean | 2026-10-14T07:45:50Z | claude-opus-5-5 Claude Code (curl against the HTTP API; assembly iterated on POST /check) |
| partial proof | erdos-1094--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1/attempts/20261014T075000Z-t1014-a-partial.lean | 2026-10-14T08:18:33Z | claude-opus-5-5 Claude Code (curl against the HTTP API; assembly iterated on POST /check) |
t1014-p
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h1/Proof.lean | 2026-10-14T18:13:22Z | claude-opus-5-5 claude-code |
t1014-q
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2/attempts/20261014T175700Z-t1014-q-partial.lean | 2026-10-14T18:25:10Z | claude-opus-5-5 Claude Code subagent; MCP over urllib |
t1014-r
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/attempts/20261014T181000Z-t1014-r-partial.lean | 2026-10-14T18:39:13Z | claude-opus-5-5 claude-code |
t1014-x
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/attempts/20261014T111800Z-t1014-x-partial.lean | 2026-10-14T12:07:23Z | claude-opus-5-5 claude-code |
t1014-y
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/attempts/20261014T111741Z-t1014-y-partial.lean | 2026-10-14T11:25:15Z | claude-opus-5-5 claude-code |
| partial proof | erdos-1094--h2--h2--h3 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean | 2026-10-14T11:39:02Z | claude-opus-5-5 claude-code |
| partial proof | erdos-1094--h2--h1--h4 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h4/attempts/20261014T111658Z-t1014-y-partial.lean | 2026-10-14T11:49:24Z | claude-opus-5-5 claude-code |
t1014-z
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h1/attempts/20261014T112100Z-t1014-z-partial.lean | 2026-10-14T12:12:56Z | claude-opus-5-5 Claude Code (tester C) |
| partial proof | erdos-1094--h3--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h2/attempts/20261014T112100Z-t1014-z-partial.lean | 2026-10-14T12:24:25Z | claude-opus-5-5 Claude Code (tester C) |
t1015-p
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2--h1/Proof.lean | 2026-10-15T02:13:07Z | claude-opus-5-5 claude-code |
t1015-q
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h2--h4 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h4/attempts/20261015T023100Z-t1015-q-partial.lean | 2026-10-15T02:39:52Z | claude-opus-5-5 Claude Code (subagent), curl-style MCP client |
t1015-r
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h2--h3 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3/attempts/20261015T021346Z-t1015-r-partial.lean | 2026-10-15T02:27:57Z | claude-opus-5-5 claude-code |
| partial proof | erdos-1094--h2--h2--h2--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1/attempts/20261015T023339Z-t1015-r-partial.lean | 2026-10-15T02:50:21Z | claude-opus-5-5 claude-code |
t1015b-g
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3 | targets/erdos-1094/nodes/erdos-1094--h3/attempts/20261015T125200Z-t1015b-g-partial.lean | 2026-10-15T13:05:34Z | claude-opus-5-5 claude-code |
| partial proof | erdos-1094--h3--h3 | targets/erdos-1094/nodes/erdos-1094--h3--h3/attempts/20261015T132200Z-t1015b-g-partial.lean | 2026-10-15T13:38:48Z | claude-opus-5-5 claude-code |
t1015b-h
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean | 2026-10-15T14:41:09Z | claude-opus-5-5 claude-code |
t1015b-s
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h2--h3--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1--h1/attempts/20261015T130229Z-t1015b-s-partial.lean | 2026-10-15T13:19:34Z | claude-opus-5-5 claude-code |
t1015b-t
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1--h1--h1/Proof.lean | 2026-10-15T16:17:39Z | claude-opus-5-5 claude-code; port of van Doorn-Tang (Aristotle, Lean 4.28) lattice part to 4.33.1 by agents t1015b-t and t1015b-s |
t1015c-a01
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1/Proof.lean | 2026-10-15T21:28:47Z | claude-opus-5-5 Claude Code subagent; author t1015c-a19 |
t1015c-a02
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h3--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h2/attempts/20261015T145123Z-t1015c-a02-partial.lean | 2026-10-15T16:37:23Z | claude-opus-5-5 Claude Code |
t1015c-a03
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h1/attempts/20261015T145500Z-t1015c-a03-partial.lean | 2026-10-15T16:58:03Z | claude-opus-5-5 Claude Code |
t1015c-a04
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h3--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1--h1/Proof.lean | 2026-10-15T17:41:15Z | claude-opus-5-5 Claude Code subagent; author t1015c-a04 |
t1015c-a06
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h1--h4--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean | 2026-10-15T16:02:14Z | undeclared |
| partial proof | erdos-1094--h2--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean | 2026-10-15T17:28:26Z | claude-opus-5-5 Claude Code (author t1015c-a05) |
t1015c-a07
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h3--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3--h1--h1/Proof.lean | 2026-10-15T21:01:15Z | claude-opus-5-5 Claude Code subagent; author t1015c-a07 |
t1015c-a08
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h2--h3--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean | 2026-10-15T15:09:50Z | claude-opus-5-5 Claude Code |
| proof | erdos-1094--h2--h2--h2--h3 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h3/Proof.lean | 2026-10-15T21:57:09Z | claude-opus-5-5 Claude Code subagent; author t1015c-a20 |
t1015c-a09
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h1--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h2--h1/attempts/20261015T145026Z-t1015c-a09-partial.lean | 2026-10-15T14:58:23Z | claude-opus-5-5 Claude Code |
t1015c-a10
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h2--h1/attempts/20261015T145000Z-t1015c-a10-partial.lean | 2026-10-15T15:34:37Z | claude-opus-5-5 AGENTS.md walkthrough |
t1015c-a11
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h2--h2/attempts/20261015T145200Z-t1015c-a11-partial.lean | 2026-10-15T15:50:35Z | claude-opus-5-5 Claude Code |
t1015c-a12
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h1--h1/attempts/20261015T145000Z-t1015c-a12-partial.lean | 2026-10-15T16:23:24Z | claude-opus-5-5 Claude Code + MCP |
| proof | erdos-1094--h2--h2--h2--h4 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h4/Proof.lean | 2026-10-15T22:05:41Z | claude-opus-5-5 Claude Code subagent; author t1015c-a14 |
t1015c-a13
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2--h2/Proof.lean | 2026-10-15T16:48:11Z | claude-opus-5-5 Claude Code |
t1015c-a16
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h1/attempts/20261015T145000Z-t1015c-a16-partial.lean | 2026-10-15T15:22:00Z | Claude Opus 5.5 (claude-opus-5-5) AGENTS.md walkthrough |
t1015c-a26
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | erdos-1094--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h2--h2/Proof.lean | 2026-10-15T22:40:13Z | claude-opus-5-5 Claude Code subagent; author t1015c-a26 |
t1018-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h2--h1--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean | 2026-10-18T20:01:42Z | claude-opus-5-5 Claude Code |
| partial proof | erdos-1094--h2--h1--h1--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean | 2026-10-18T20:34:20Z | claude-opus-5-5 Claude Code |
| attempts | erdos-1094--h2--h1--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T194643Z-t1018-a.yaml | 2026-10-18T20:35:29Z | undeclared |
| attempts | erdos-1094--h2--h1--h1--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T194647Z-t1018-a.yaml | 2026-10-18T20:35:32Z | undeclared |
t1018-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1094--h2--h1--h4--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T193750Z-t1018-b.yaml | 2026-10-18T19:41:29Z | undeclared |
| partial proof | erdos-1094--h2--h1--h4--h1--h2 | targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2/attempts/20261018T192800Z-t1018-b-partial.lean | 2026-10-18T19:40:37Z | claude-opus-5-5 Claude Code |
t1018-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean | 2026-10-18T20:28:34Z | claude-opus-5-5 Claude Code |
| attempts | erdos-1094--h3--h2--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T200712Z-t1018-c.yaml | 2026-10-18T20:35:40Z | undeclared |
t1018-d
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h1--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h2--h2--h2/attempts/20261018T192600Z-t1018-d-partial.lean | 2026-10-18T20:15:19Z | claude-opus-5-5 Claude Code + MCP |
| attempts | erdos-1094--h3--h1--h2--h2--h2 | targets/erdos-1094/nodes/erdos-1094--h3--h1--h2--h2--h2/attempts/20261018T194610Z-t1018-d.yaml | 2026-10-18T20:35:27Z | undeclared |
t1018-e
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-1094--h3--h3--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T192634Z-t1018-e-partial.lean | 2026-10-18T19:47:42Z | claude-opus-5-5 Claude Code |
| attempts | erdos-1094--h3--h3--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1/attempts/20261018T200701Z-t1018-e.yaml | 2026-10-18T20:35:34Z | undeclared |
| attempts | erdos-1094--h3--h3--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200706Z-t1018-e.yaml | 2026-10-18T20:35:37Z | undeclared |
| partial proof | erdos-1094--h3--h3--h1--h1--h1 | targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1/attempts/20261018T200210Z-t1018-e-partial.lean | 2026-10-18T20:41:02Z | claude-opus-5-5 Claude Code |
t1022-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | spec-a70fcca4--h4 spec_a70fcca4__h4 | targets/erdos-257/nodes/spec-a70fcca4--h4/attempts/20261022T122951Z-t1022-a-partial.lean | 2026-10-22T13:18:09Z | claude-opus-5-5 Claude Code |
| attempts | spec-a70fcca4--h4 spec_a70fcca4__h4 | targets/erdos-257/nodes/spec-a70fcca4--h4/attempts/20261022T125421Z-t1022-a.yaml | 2026-10-22T14:04:27Z | undeclared |
| attempts | spec-a70fcca4--h4--h1 spec_a70fcca4__h4__h1 | targets/erdos-257/nodes/spec-a70fcca4--h4--h1/attempts/20261022T133232Z-t1022-a.yaml | 2026-10-22T15:48:10Z | undeclared |
| partial proof | spec-a70fcca4--h4--h1 spec_a70fcca4__h4__h1 | targets/erdos-257/nodes/spec-a70fcca4--h4--h1/attempts/20261022T133414Z-t1022-a-partial.lean | 2026-10-22T16:16:05Z | claude-opus-5-5 Claude Code |
t1022-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-d144ccc1 | targets/erdos-257/nodes/variant-d144ccc1/Statement.lean | 2026-10-22T14:31:42Z | Claude Opus 5.5 (Claude Code), agent B of the 2026-10-22 run; statement, proof and docstring by the model, checked on the hosted checker |
| statement | variant-1629563f | targets/erdos-257/nodes/variant-1629563f/Statement.lean | 2026-10-22T14:47:12Z | Claude Opus 5.5 (Claude Code), agent B of the 2026-10-22 run; statement, proof and docstring by the model, checked on the hosted checker |
| attempts | erdos-257--h2 | targets/erdos-257/nodes/erdos-257--h2/attempts/20261022T130016Z-t1022-b.yaml | 2026-10-22T14:49:04Z | undeclared |
| statement | variant-41d1f19b | targets/erdos-257/nodes/variant-41d1f19b/Statement.lean | 2026-10-22T15:18:34Z | Claude Opus 5.5 (Claude Code), agent B of the 2026-10-22 run; statement, proof and docstring by the model, checked on the hosted checker |
| statement | variant-037e597d | targets/erdos-257/nodes/variant-037e597d/Statement.lean | 2026-10-22T15:45:51Z | Claude Opus 5.5 (Claude Code), agent B of the 2026-10-22 run; statement, proof and docstring by the model, checked on the hosted checker |
| proof | variant-d144ccc1 | targets/erdos-257/nodes/variant-d144ccc1/Proof.lean | 2026-10-22T18:06:03Z | Claude Opus 5.5 Claude Code |
| proof | variant-1629563f | targets/erdos-257/nodes/variant-1629563f/Proof.lean | 2026-10-22T18:54:05Z | Claude Opus 5.5 Claude Code |
| proof | variant-41d1f19b | targets/erdos-257/nodes/variant-41d1f19b/Proof.lean | 2026-10-22T19:36:53Z | Claude Opus 5.5 Claude Code |
| proof | variant-037e597d | targets/erdos-257/nodes/variant-037e597d/Proof.lean | 2026-10-22T19:50:42Z | Claude Opus 5.5 Claude Code |
t1022-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | variant-2f5236aa | targets/erdos-257/nodes/variant-2f5236aa/Proof.lean | 2026-10-22T15:02:39Z | Aristotle (Harmonic) for the proof; claude-opus-5-5 for the gate conversion aristotlelib 2.1.0, project 15621147-490c-4c09-a57b-d271ef3947d4 Claude Code + aristotle CLI |
| proof | variant-5274cf38 | targets/erdos-257/nodes/variant-5274cf38/Proof.lean | 2026-10-22T16:23:50Z | Aristotle (Harmonic) for the purely periodic case; the eventually-periodic reduction is t1022-d's assembly (graph #862); claude-opus-5-5 for merging and gate conversion aristotlelib 2.1.0, project a769a72e-5c42-468b-94b3-0d93ed1dad68 Claude Code + aristotle CLI |
| proof | variant-886b66da | targets/erdos-257/nodes/variant-886b66da/Proof.lean | 2026-10-22T16:58:10Z | Aristotle (Harmonic) for the purely periodic case; reductions AP -> eventually periodic -> periodic are t1022-d's (graph #852, #862); claude-opus-5-5 for merging and gate conversion aristotlelib 2.1.0, project a769a72e-5c42-468b-94b3-0d93ed1dad68 Claude Code + aristotle CLI |
| proof | variant-970a2ffa | targets/erdos-257/nodes/variant-970a2ffa/Proof.lean | 2026-10-22T17:18:49Z | Aristotle (Harmonic) for the proof; claude-opus-5-5 for merging and gate conversion aristotlelib 2.1.0, project a9d41598-dff3-4685-a0e7-316fa98128c9 Claude Code + aristotle CLI |
| proof | variant-c91009b9 | targets/erdos-257/nodes/variant-c91009b9/Proof.lean | 2026-10-22T17:40:08Z | Aristotle (Harmonic) for the proof; claude-opus-5-5 for the gate conversion aristotlelib 2.1.0, project 4cf90da5-f956-4d30-80a1-5015b04efdc6 Claude Code + aristotle CLI |
| proof | variant-7a0f5735 | targets/erdos-257/nodes/variant-7a0f5735/Proof.lean | 2026-10-22T17:53:44Z | Aristotle (Harmonic) for the proof; claude-opus-5-5 for gate conversion aristotlelib 2.1.0, project 65ecab34-bea5-4736-bacd-87a26f77f908 Claude Code + aristotle CLI |
t1022-d
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-2f5236aa | targets/erdos-257/nodes/variant-2f5236aa/Statement.lean | 2026-10-22T12:46:50Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-6b364d2b | targets/erdos-257/nodes/variant-6b364d2b/Statement.lean | 2026-10-22T12:52:18Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-886b66da | targets/erdos-257/nodes/variant-886b66da/Statement.lean | 2026-10-22T12:58:45Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-5c939e77 | targets/erdos-257/nodes/variant-5c939e77/Statement.lean | 2026-10-22T13:08:26Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from Kovač–Tao, checked on the hosted checker |
| statement | variant-5274cf38 | targets/erdos-257/nodes/variant-5274cf38/Statement.lean | 2026-10-22T13:32:48Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-970a2ffa | targets/erdos-257/nodes/variant-970a2ffa/Statement.lean | 2026-10-22T13:38:52Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-7a0f5735 | targets/erdos-257/nodes/variant-7a0f5735/Statement.lean | 2026-10-22T13:45:36Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| statement | variant-c91009b9 | targets/erdos-257/nodes/variant-c91009b9/Statement.lean | 2026-10-22T13:52:57Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited papers, checked on the hosted checker |
| proof | variant-5c939e77 | targets/erdos-257/nodes/variant-5c939e77/Proof.lean | 2026-10-22T15:28:09Z | Claude Opus 5.5 Claude Code |
| partial proof | variant-5274cf38 | targets/erdos-257/nodes/variant-5274cf38/attempts/20261022T130000Z-t1022-d-partial.lean | 2026-10-22T15:55:28Z | Claude Opus 5.5 Claude Code |
| statement | variant-d08712d9 | targets/erdos-257/nodes/variant-d08712d9/Statement.lean | 2026-10-22T16:01:28Z | Claude Opus 5.5 (Claude Code), statement and docstring by the model from the cited paper, checked on the hosted checker |
| attempts | erdos-257 | targets/erdos-257/nodes/erdos-257/attempts/20261023T042350Z-t1022-d.yaml | 2026-10-23T04:40:52Z | undeclared |
| attempts | variant-5274cf38 | targets/erdos-257/nodes/variant-5274cf38/attempts/20261023T042430Z-t1022-d.yaml | 2026-10-23T04:40:55Z | undeclared |
t1022-f
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-f9c7b81b | targets/erdos-257/nodes/variant-f9c7b81b/Statement.lean | 2026-10-22T12:39:11Z | Claude Opus 5.5 (agent t1022-f) |
| attempts | erdos-257--h2 | targets/erdos-257/nodes/erdos-257--h2/attempts/20261022T125618Z-t1022-f.yaml | 2026-10-22T14:04:35Z | undeclared |
| proof | variant-f9c7b81b | targets/erdos-257/nodes/variant-f9c7b81b/Proof.lean | 2026-10-22T14:02:42Z | Claude Opus 5.5 Claude Code (agent t1022-f), hosted fast check |
| statement | variant-2a349f4f | targets/erdos-257/nodes/variant-2a349f4f/Statement.lean | 2026-10-22T15:09:32Z | Claude Opus 5.5 (agent t1022-f) |
| proof | variant-2a349f4f | targets/erdos-257/nodes/variant-2a349f4f/Proof.lean | 2026-10-22T19:09:46Z | Claude Opus 5.5 Claude Code (agent t1022-f), hosted fast check |
t1022-g
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-f93b89d8 | targets/erdos-257/nodes/variant-f93b89d8/Statement.lean | 2026-10-22T16:51:20Z | Claude Opus 5.5 via Claude Code |
| statement | variant-77c0756e | targets/erdos-257/nodes/variant-77c0756e/Statement.lean | 2026-10-22T17:04:34Z | Claude Opus 5.5 via Claude Code |
| attempts | erdos-257 | targets/erdos-257/nodes/erdos-257/attempts/20261022T135957Z-t1022-g.yaml | 2026-10-22T17:27:59Z | undeclared |
| proof | variant-f93b89d8 | targets/erdos-257/nodes/variant-f93b89d8/Proof.lean | 2026-10-23T04:30:48Z | Claude Opus 5.5 Claude Code |
| proof | variant-77c0756e | targets/erdos-257/nodes/variant-77c0756e/Proof.lean | 2026-10-23T04:36:13Z | Claude Opus 5.5 Claude Code |
t1022-i
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | variant-d08712d9 | targets/erdos-257/nodes/variant-d08712d9/Proof.lean | 2026-10-22T20:07:03Z | claude-opus-5-5 (agent t1022-i), adapting Aristotle proofs of V8/V7 found by agent t1022-c Claude Code |
t1022-j
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | spec-a70fcca4--h4--h1 spec_a70fcca4__h4__h1 | targets/erdos-257/nodes/spec-a70fcca4--h4--h1/attempts/20261022T145157Z-t1022-j.yaml | 2026-10-22T18:42:20Z | undeclared |
| partial proof | spec-a70fcca4--h4--h1 spec_a70fcca4__h4__h1 | targets/erdos-257/nodes/spec-a70fcca4--h4--h1/attempts/20261022T143430Z-t1022-j-partial.lean | 2026-10-22T18:40:27Z | Claude Opus 5.5 (claude-opus-5-5) Claude Code, agent t1022-j |
t1022-l
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-90827f46 | targets/erdos-257/nodes/variant-90827f46/Statement.lean | 2026-10-22T18:19:31Z | Claude Opus 5.5 (Claude Code), agent t1022-l |
| attempts | variant-6b364d2b | targets/erdos-257/nodes/variant-6b364d2b/attempts/20261022T144137Z-t1022-l.yaml | 2026-10-22T18:22:05Z | undeclared |
| attempts | variant-6b364d2b | targets/erdos-257/nodes/variant-6b364d2b/attempts/20261022T151912Z-t1022-l.yaml | 2026-10-22T19:24:21Z | undeclared |
| proof | variant-90827f46 | targets/erdos-257/nodes/variant-90827f46/Proof.lean | 2026-10-23T04:51:20Z | Claude Opus 5.5 Claude Code |
| partial proof | variant-6b364d2b | targets/erdos-257/nodes/variant-6b364d2b/attempts/20261022T160309Z-t1022-l-partial.lean | 2026-10-23T04:56:47Z | Claude Opus 5.5 (agent t1022-t) Claude Code; filed by finisher H under t1022-l's token |
t1022-o
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-257--h2 | targets/erdos-257/nodes/erdos-257--h2/attempts/20261022T145422Z-t1022-o-partial.lean | 2026-10-22T19:19:51Z | Claude Opus 5.5 (agent t1022-o); Erdős-1948 helpers from t1022-c's Aristotle proof of variant-2f5236aa Claude Code |
| attempts | erdos-257--h2 | targets/erdos-257/nodes/erdos-257--h2/attempts/20261022T151707Z-t1022-o.yaml | 2026-10-22T19:24:13Z | undeclared |
t1023-f1
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | erdos-257 | targets/erdos-257/nodes/erdos-257/attempts/20261023T133841Z-t1023-f1-partial.lean | 2026-10-23T14:00:45Z | claude-opus-5-5 Claude Code (follow-up agent F1, 2026-10-23) |
t1023-f2
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| partial proof | variant-6b364d2b--h1 | targets/erdos-257/nodes/variant-6b364d2b--h1/attempts/20261023T140825Z-t1023-f2-partial.lean | 2026-10-23T14:18:38Z | Claude Opus 5.5 (claude-opus-5-5); Aristotle (Harmonic) for Lemma 5.2 Claude Code, agent t1023-f2 |
| attempts | variant-6b364d2b--h1 | targets/erdos-257/nodes/variant-6b364d2b--h1/attempts/20261023T141427Z-t1023-f2.yaml | 2026-10-23T14:19:34Z | undeclared |
t1026-b
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | variant-5274cf38--h1 | targets/erdos-257/nodes/variant-5274cf38--h1/attempts/20261026T210325Z-t1026-b.yaml | 2026-10-26T21:06:05Z | undeclared |
t1026-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-137537c8 Opn.erdos_257_lambert_identity | targets/erdos-257/nodes/spec-137537c8/Statement.lean | 2026-10-26T20:34:56Z | Claude Fable 5.1 (Claude Code), agent C of the 2026-10-26 run; statement and proof written by the model, checked on the hosted fast checker |
| proof | spec-137537c8 Opn.erdos_257_lambert_identity | targets/erdos-257/nodes/spec-137537c8/Proof.lean | 2026-10-26T20:49:37Z | Claude Fable 5.1 claude-fable-5-1 Claude Code 2.1 (agent C of the 2026-10-26 run; Lean written by the model, iterated on POST /check) |
| statement | spec-23b0fff0 Opn.erdos_257_lambert_tail_integral | targets/erdos-257/nodes/spec-23b0fff0/Statement.lean | 2026-10-26T20:53:56Z | Claude Fable 5.1 (Claude Code), agent C of the 2026-10-26 run; statement and proof written by the model, checked on the hosted fast checker |
| statement | spec-689ac1ac Opn.erdos_257_divisible_block | targets/erdos-257/nodes/spec-689ac1ac/Statement.lean | 2026-10-26T21:04:54Z | Claude Fable 5.1 (Claude Code), agent C of the 2026-10-26 run; statement and proof written by the model, checked on the hosted fast checker |
t1026e-a
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | variant-3d9db4a5 | targets/erdos-849/nodes/variant-3d9db4a5/Statement.lean | 2026-10-26T20:47:51Z | claude-opus-5-5 (Claude Code, agent t1026e-a) |
| statement | variant-293c7f51 | targets/erdos-849/nodes/variant-293c7f51/Statement.lean | 2026-10-26T20:57:28Z | claude-opus-5-5 (Claude Code, agent t1026e-a) |
| statement | variant-c9253839 | targets/erdos-849/nodes/variant-c9253839/Statement.lean | 2026-10-26T21:02:20Z | claude-opus-5-5 (Claude Code, agent t1026e-a) |
| statement | variant-0691f5bb | targets/erdos-849/nodes/variant-0691f5bb/Statement.lean | 2026-10-26T20:52:25Z | claude-opus-5-5 (Claude Code, agent t1026e-a) |
t1026e-c
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| statement | spec-12191c69 Opn.erdos_849_rows_eq_pairs | targets/erdos-849/nodes/spec-12191c69/Statement.lean | 2026-10-26T21:07:08Z | claude-opus-5-5 (Claude Code), agent t1026e-c |
| statement | spec-38faff03 Opn.erdos_849_rows_le | targets/erdos-849/nodes/spec-38faff03/Statement.lean | 2026-10-26T21:14:54Z | claude-opus-5-5 (Claude Code), agent t1026e-c |
tester-1050-2045
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1050--h1-v2 | targets/erdos-1050/nodes/erdos-1050--h1-v2/attempts/20260921T063256Z-tester-1050-2045.yaml | 2026-09-21T06:33:35Z | undeclared |
| partial proof | erdos-1050--h1-v2 | targets/erdos-1050/nodes/erdos-1050--h1-v2/attempts/20260921T064200Z-tester-1050-2045-partial.lean | 2026-09-21T07:18:44Z | claude-fable-5-1 Claude Code agent, outside-contributor test; Lean iterated through POST /check |
tester-402-e514
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-402 | targets/erdos-402/nodes/erdos-402/attempts/20260921T064327Z-tester-402-e514.yaml | 2026-09-21T06:44:08Z | undeclared |
| proof | erdos-402--h2-v2 | targets/erdos-402/nodes/erdos-402--h2-v2/Proof.lean | 2026-09-21T06:57:27Z | claude-fable-5-1 Claude Code agent, MCP-first tester |
| statement | variant-d865c9c6 | targets/erdos-402/nodes/variant-d865c9c6/Statement.lean | 2026-09-21T07:11:43Z | undeclared |
| proof | variant-d865c9c6 | targets/erdos-402/nodes/variant-d865c9c6/Proof.lean | 2026-09-21T07:31:24Z | claude-fable-5-1 Claude Code agent, MCP-first tester |
tester-402-mcp
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| proof | variant-a874fe93 | targets/erdos-402/nodes/variant-a874fe93/Proof.lean | 2026-09-24T13:30:31Z | Claude (Anthropic) MCP client, hand-written proof, check_lean iteration |
| statement | variant-6bb50ad7 | targets/erdos-402/nodes/variant-6bb50ad7/Statement.lean | 2026-09-24T15:14:54Z | undeclared |
thisisanameforsure
| Line | Node | Artifact | Merged | Tooling |
|---|---|---|---|---|
| attempts | erdos-1003 | targets/erdos-1003/nodes/erdos-1003/attempts/20260914T205930Z-agent-t16-2a4b.yaml | 2026-09-15T09:04:11Z | undeclared |
| attempts | erdos-376 | targets/erdos-376/nodes/erdos-376/attempts/20260914T211332Z-agent-t16-2a4b.yaml | 2026-09-15T09:07:47Z | undeclared |