Erdős problem · #742 · Murty–Simon conjecture · AMS 5 · open

Erdős 742

A diameter-2-critical graph on n vertices has at most ⌊n²/4⌋ edges. A repository claims a complete Lean proof; SISO's review lane got the statement to match Formal Conjectures and the dependency audit to pass, and the theorem did not compile. No kernel or axiom receipt exists, so the state here is unverified.

research questionproof state · unverified REVIEW-742 · partial laptop lane frozen 30 Aug ERDOS-LEAD · mini · idle

Problem statement Approach · reductions Certificate · replay status Compute spent · host Decision log What would close it

4approach steps 5compute facts 5decision-log lines 4repos

Problem statement

from the Formal Conjectures file fetched at review time (sha256 25f7c5cd…)

Murty–Simon Conjecture. Let G be a graph on n vertices with diameter 2 such that deleting any edge increases the diameter. Is it true that G has at most ⌊n²/4⌋ edges? Equality is conjectured to hold for the complete balanced bipartite graph K_{⌈n/2⌉,⌊n/2⌋}.

formal statement: theorem erdos_742 : answer(sorry) ↔ ∀ (V : Type*) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj], IsDiameter2Critical G → G.edgeFinset.card ≤ (Fintype.card V) ^ 2 / 4
definition: IsDiameter2Critical G := G.diam = 2 ∧ ∀ e ∈ G.edgeSet, (G.deleteEdges {e}).diam ≠ 2
category: research open · AMS 5 (Formal Conjectures tag)
resolved up to: a finite check: Fan [Fa87] n ≤ 24 and n = 26; Füredi [Fü92] all sufficiently large n
lane brief: targets/742/README.md: "audit and extend proof-logging SAT work at order 25. Preserve CNF identity, solver version, proof log, independent replay, and any decoded graph."

we need one for each ERDOS question we need one for each god question we need one for each agent zero, we need one for each research doc, we need one for each project one pagerShaan → AGENT-ZERO · 00_AGENT_ZERO/source/2026-09-06-1650-… · 6 Sep 16:50

Approach · reductions

what the fleet chose to do and why

1
Admit 742 first as a bounded falsification/certification job admittedaudits/easiest-targets.md: "the practical frontier is one finite order (25), the SAT input and candidate checker are public, and a SAT witness would be a genuine counterexample"
2
Then a repository claimed a complete Lean proof claimaudits/solver-repositories.md §742: Erdos742.lean 173 KB, Equality.lean 300 KB, Erdos742Full.lean 474 KB, two papers; "no lakefile.lean, lean-toolchain, workflow, build script, certificate manifest, or pinned dependency file"
3
Goal /review-742-proof goal"Wrap the pinned Erdos742/Erdos742 sources in the smallest reproducible Lean project, compile the headline theorem, print its transitive axioms, and determine whether any sorryAx or unstated hypothesis reaches the result." PASS requires a reproducible build plus statement-fidelity and axiom receipts.
4
Reusable SAT path kept availableleansolving/leansms (Apache-2.0) MurtySimon encoder, lake exe murty-simon-generate <n>: verified CNF/LRAT impossibility proofs for finite orders; restricted LRAT classes exist upstream (edisonymy/erdos-lean-research experiments/erdos742)

Pindetached checkout at 814289f2, source sha256 recorded

Matchstatement against Formal Conjectures 742 (fetched, sha256 recorded)

Buildsmallest wrapper project: lakefile, toolchain v4.33.0-rc1, Main.lean with #print axioms

Audittransitive axioms for sorryAx, custom axioms, native_decide

Certificate · replay status

proof state only from a receipt; the claim ceiling of this page

proof stateunverifiedno kernel or axiom receipt; "classify the claim as candidate-proof/blocked, not kernel-checked or solved" (HANDOFF.md)

statement fidelitypassedIsDiameter2Critical and erdos_742 agree textually with Formal Conjectures after removing answer(sorry)

static sorry auditpassed · 1 literal sorry, statically unreachabledependency-audit.txt; MAC-MINI handoff: "no kernel/axiom receipt exists"

buildexit 124 · timed out in dependency acquisitionlake update tried to clone Mathlib; a path-dependency retry (647's mathlib) was stopped

replayable certificatenoneno LRAT/DRAT for order 25 in this workspace; upstream restricted classes are not this claim

independent review (Sol)not runSol is reserved for a genuine proof boundary; none reached

Gate	Command	Result	Receipt
checkout pinned	`git -C Erdos742 rev-parse HEAD`	814289f2…	HANDOFF.md verify line; status --short empty
source hash	`sha256 Erdos742/Erdos742.lean`	355a8539…	HANDOFF.md evidence line
reference statement	`curl … formal-conjectures/…/742.lean`	exit 0	`formal-conjectures-fetch.exit` = 0; sha256 25f7c5cd…
bounded build	`timeout 10s … lake build Erdos742`	exit 124	`build-timeout.exit` = 124; `build.log` 15 lines, cloning aesop/Qq/batteries
axiom print	`lake env lean Main.lean → #print axioms Erdos742.erdos_742`	not reached	Main.lean present; never executed

replay command · what a certificate would take

cd SISO_Research/erdos/targets/742/runs/proof-review
# obtain Mathlib at exactly ae0d973 without touching Erdos742/, point lake-manifest at it, then
elan run leanprover/lean4:v4.33.0-rc1 lake build Erdos742
elan run leanprover/lean4:v4.33.0-rc1 lake env lean Main.lean   # must print axioms of Erdos742.erdos_742

From HANDOFF.md "Smallest next action". Until the second command completes and its transitive axioms are inspected for sorryAx, custom axioms and native_decide, the chip above stays amber.

Compute spent · host

what is measured, what is not

1review run (proof-review)

10 sbounded build budget · exit 124

0kernel-checked theorems

2historical ChatGPT turns recovered · 240 m + 33 m

—tokens · not measured

host: laptop (MacBook), frozen 30 Aug 16:35: "Freeze all laptop proof/Lean compute and move the programme to a dedicated Mac Mini workspace"
next host: Mac Mini M4 · 16 GB (ESTATE.md); ERDOS-LEAD seat present in atlas/now.json, node mini, idle
toolchain: leanprover/lean4:v4.33.0-rc1 installed; Mathlib ae0d973 named by upstream comments, not acquired
what is not measured: wall time of the lane, tokens, CPU; the workspace has no run ledger for 742 (only the exit-code receipts above)
historical: audits/connector-recovery-2026-09-06/erdos-742-historical-chat.md: a recovered ChatGPT thread ("Worked for 240m 4s", "I did not finish a full proof"); prose, not a certificate

Decision log

DECISION-LOG.html and CHECKPOINT-2026-08-30.html, verbatim lines as facts

fact · has a receiptproposal · not yet

WIN: #23 exact replay passed; #647 bounded C slice passed; #742 and #848 release blockers were localized.DECISION-LOG.html · 30 Aug 2026

DECISION: Freeze all laptop proof/Lean compute and move the programme to a dedicated Mac Mini workspace.DECISION-LOG.html · 30 Aug 2026

TRAP: A successful arithmetic replay is not a theorem-interface proof; a repository claiming kernel closure is not reproducible when its own manifest gate fails.DECISION-LOG.html · 30 Aug 2026

LEARN: Run release-integrity and dependency-lock gates before expensive proof review; keep intentional axioms separate from certified finite evidence.DECISION-LOG.html · 30 Aug 2026

Hard-won traps: Do not accept certificate arithmetic as semantic theorem validation. Do not accept a Lean claim without a pinned dependency lock and executed axiom audit. Do not let a returned worker leave an orphaned Lean process.CHECKPOINT-2026-08-30.html · 30 Aug 2026 16:35

Exactly one resume step: a fresh Mini Codex reads the handoff, then resumes the interrupted #23 Sol interface review before admitting any new proof compute.MAC-MINI-HANDOFF-2026-08-30.md §"Exactly one resume step"; 742 waits behind it

Limits

Proof state on this page comes only from targets/742/runs/proof-review receipts and the 30 Aug audits; no handoff sentence upgrades it.
The upstream repository's own claim ("only ordinary Lean axioms, no sorryAx") is quoted by audits/solver-repositories.md and is not a receipt.
The erdos workspace sits inside SISO_Workspace (outer repo untracked); no commit hash pins these files.

Version

proof-review · 30 Aug 16:22

HANDOFF.md status: done · result: PARTIAL

What would close it

1
Kernel-checked build of erdos_742 with an executed axiom print closes the claimthe two commands in §03 complete on a clean machine with Mathlib ae0d973; transitive axioms contain no sorryAx, custom axiom or native_decide
2
Or a finite counterexample at order 25 closes the conjecturea SAT witness decoded to a diameter-2-critical graph with more than ⌊625/4⌋ = 156 edges (easiest-targets: "would settle the conjecture negatively")
3
Or a replayable LRAT/DRAT for order 25 finiteextends Fan's finite check by one order; a finite result, not the conjecture (README "Completion standard")
4
Cold Sol review at the boundary gateonly once one of the above exists (AGENTS.md operating rules)

Repos · certificate files

the erdos workspace (inside SISO_Workspace, not a git repo of its own) and the pinned upstreams

SISO_Research/erdos

no public locator

private

— (inside SISO_Workspace; outer repo untracked) branch

AGENTS.md · manager/{CHARTER,launch-board}.md · goals/ · targets/742/runs/proof-review/ (wrapper project, logs, exit receipts, dependency-audit.txt, pinned Erdos742/) · audits/ · DECISION-LOG.html · CHECKPOINT-2026-08-30.html · MAC-MINI-HANDOFF-2026-08-30.md

workspaceSISO

No public payload

Erdos742/Erdos742

https://github.com/Erdos742/Erdos742

public

main branch head 814289f 2026-08-10 07:36 UTC+07

The claimed proof: Erdos742.lean (173 KB), Equality.lean, Erdos742Full.lean, two papers. No lakefile, toolchain, lock or manifest.

no declared licence

Open repo

google-deepmind/formal-conjectures

https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/742.lean

public

main branch

The reference statement (fetched at review, sha256 25f7c5cd…).

Apache-2.0

Open repo

leansolving/leansms

https://github.com/leansolving/leansms

public

head f5e9528

MurtySimon encoder; verified CNF/LRAT impossibility proofs for finite orders (the order-25 path).

Apache-2.0

Open repo

Fleet · seats

the four problems as the 30 Aug handoff observed them

#	Lane	Observed status (30 Aug)	Durable evidence
742	REVIEW-742 · luna-review-742	PARTIAL statement/static dependency audit passed, theorem did not compile	`targets/742/runs/proof-review/HANDOFF.md`
23	VERIFY-23 · luna-verify-23 · SOL-REVIEW-23	PARTIAL exact arithmetic replay passed; six mathematical interfaces not discharged; Sol review interrupted, no verdict	`targets/23/runs/baseline/HANDOFF.md`
647	REPLAY-647 · luna-replay-647	handoff C validation slice passed (55 closed, 41 open residues, one intentional Stage-1 axiom); Lean replay interrupted	`targets/647/runs/baseline/HANDOFF.md`
848	VERIFY-848 · luna-verify-848	PARTIAL fast verifier passed; kernel-package public gate failed (PDF bytes/hash disagree with manifest)	`targets/848/runs/baseline/HANDOFF.md`

root Codex · Erdős manager (laptop, frozen)luna-review-742 · partialsol · reserved, not runERDOS-LEAD · mini · idle

Attempts

upstreamreview lanedecisionsdocshis words

Mind map

problem → reductions → repos → gates

Reductions3

Repos3

Gates4

Hosts2

Each leaf links to its record. Branches are laid out by subtree size, not by hand.

Agent entry

SISO_Research/erdos/AGENTS.md → MAC-MINI-HANDOFF-2026-08-30.md → tasks/TASKS.json → SISO_Research/erdos/targets/742/runs/proof-review/HANDOFF.md

cat SISO_Research/erdos/targets/742/runs/proof-review/HANDOFF.md
cat SISO_Research/erdos/targets/742/runs/proof-review/build-timeout.exit # 124
jq '.tasks[]|select(.id=="REVIEW-742")' SISO_Research/erdos/tasks/TASKS.json
shasum -a 256 SISO_Research/erdos/targets/742/runs/proof-review/Erdos742/Erdos742.lean # 355a8539…

Agent entry

Read first: SISO_Research/erdos/AGENTS.md → MAC-MINI-HANDOFF-2026-08-30.md → tasks/TASKS.json → SISO_Research/erdos/targets/742/runs/proof-review/HANDOFF.md
Owner: Erdős manager (root Codex, frozen) · ERDOS-LEAD on the Mini, idle · last writeback 30 Aug 16:35 (handoff) · 6 Sep 04:32 (recovery audit)
Done when: Open this page and see the problem, the proof-logging status (unverified, amber: statement audit passed, build exit 124, no axiom receipt) and the replay command with the receipt files it would produce.

Problem statement

Approach · reductions

Certificate · replay status

Compute spent · host

Decision log

What would close it

Repos · certificate files

Fleet · seats

Attempts

Mind map

Links out

Agent entry