# AI provenance: The book Ramsey number R(B_57, B_58) = 231

Authors: Deep Bhattacharjee. No AI system is an author or contributor.

## How the work was produced

Deep Bhattacharjee chose the problem and directed the work. Claude (Anthropic), through Claude Code, wrote and ran the search that found the graph, wrote the independent C and Python checks and the Lean 4 formalisation, and drafted the text, which the author reviewed and edited.

## How the results are checked

The paper proves the lower bound by hand: both book conditions reduce to one inequality per nonzero residue of Z_115, and a table lists the 57 values that matter. Two independently written programs (C and Python) recount the common neighbours and common non-neighbours of all 26,335 pairs of vertices. The Lean 4 kernel checks the graph on every pair (`decide +kernel`, no `native_decide`) and proves the upper bound from Goodman's count; the final theorem `book_ramsey_58 : IsBookRamsey 57 58 231` depends only on propext, Classical.choice and Quot.sound.

## What is not claimed

Wesley's conjecture is not claimed; for n <= 100 the values 59, 60, 64, 65, 68, 72, 73, 76, 78, 80, 81, 84, 88, 89, 92, 93, 94, 96 and 100 stay open.

## Labels given on the Hexagon form

- Text of the contribution: primarily AI-generated (to be confirmed by the author).
- Human understanding at submission: some parts, but not all, checked and understood by a human (to be confirmed by the author).

## Where everything is

Release v2.1.0: https://github.com/creelie/Breakthrough-problems-2/releases/tag/v2.1.0. The manuscript's declaration on generative AI says the same.