[abu-aska]

Summary

This PR adds a collection of mathematics produced by Claude. Every result has a complete Lean 4 proof, checked by the kernel against a fixed statement and using only the standard axioms. The collection's page is RESULTS.md. README.md stays main's hub page, with one row added to its projects table. Whether the collection stays in this repository or moves to its own is open for the maintainers.

153 results. Each passed an adversarial integrity referee. For open problems, a novelty referee also searched the literature, and where the referees disagreed the more conservative classification was used.

Classification	Count
New result (conjecture settled; no earlier resolution found)	74
First formal proof of a known result	55
Independent formal proof (a Lean proof of it already exists elsewhere)	18
Misformalization found (the upstream statement does not match the problem)	6

How hard were the new results? All 74 are routine. An independent assessor judged each one, and a second assessor challenged every "substantial" verdict. Routine means a short or standard argument, something that follows from material already in the OEIS entry or the literature, or a finite search. Most of these conjectures stayed open for lack of attention, not because they were hard. Each result page gives the assessor's reasons.

A278212 (Kagey's bishop/queen mobility) was rated substantial until 29 Oct. Its queen bound turned out to have a one-page charging proof, written up in results/oeis-a275815/short-proof.md. That proof is not formalized; the Lean proofs use computer-found LP-dual certificates. Two independent agents checked it, one by hand and one by searching for counterexamples exhaustively and at random, and both found it valid for every n ≥ 8.

Where the statements come from

• Third-party (43 results): google-deepmind/formal-conjectures at pinned commit c77fdd4. Checked syntactically by #math0_proves, #math0_refutes, #math0_answers and #math0_refutes_every_answer. Every "open" item settled there had already been resolved elsewhere, or was a misformalization.
• Formalized by math0 (110 results): conjectures left in OEIS entries about series, awkward fractions and irregular shapes. Each statement's definitions are kernel-checked against the OEIS data. A separate agent reviews it for fidelity, it is frozen by hash, and only then does a prover try to settle it (#math0_settles). Fidelity is a judgement, not a machine check, so every result page quotes the OEIS text.
  • Review packets: review/fidelity/ holds 11 packets of 10 statements each. An adversarial agent prepared them for human review: each entry shows the OEIS text beside the Lean statement, with a plain-English reading and any points to check.
  • What that pass found: no unfaithful or questionable statement, and 15 minor points, listed first in the index.
  • Human review: none of these statements has had one yet.

96 results have a proofread LaTeX manuscript in results/<slug>/.

Verification (changed in response to review)

• No build cache. lean.yml rebuilds every math0 module from scratch on every run. Only Mathlib's prebuilt oleans are fetched. Modules build two at a time with swap, because the heaviest proof files need up to 8 GB each. The run fails unless exactly one statement check runs per catalogue entry.
• Freeze rules. scripts/check_freeze.py enforces them:
  • frozen hashes must match;
  • FROZEN.sha256 is append-only;
  • every math0 statement must be frozen;
  • for new results, the statement must be committed strictly before its proof. CI now checks this order from git for the 16 results added since 26 Oct.
  • The 94 statements frozen before this rule were committed together with their proofs. They are listed in FROZEN_WITH_PROOF.txt, and for them the order is recorded only in the pipeline's logs.
• Audit tests. tests/audit/ holds eleven files the audit must reject and one it must accept. CI runs them.
• Kernel replay. kernel-replay.yml replays every Math0 module through leanchecker in 4 shards and runs leanprover-community/axiom-audit. A running replay is never cancelled by a newer push.

Test plan

• On the current head 140e4ff: the uncached build (153 distinct statement checks), all four leanchecker shards and axiom-audit passed.
• scripts/test_audit.sh: 11 of 11 rejected, 1 of 1 accepted.
• scripts/check_freeze.py --base origin/main --order passes, with the order verified for 16 new results.

Open for the maintainers

• Should this PR be split into infrastructure, the formal-conjectures track and frontier batches? The review packets could serve as the batches.
• Keep the committed PDFs, or build them in CI and attach them to releases?
• Should the collection stay in this repository, or move to its own?
• Who does the human fidelity review of the 110 math0-formalized statements, using review/fidelity/?
• Who should own lean/Math0/Statements/** in CODEOWNERS?

🤖 Generated with Claude Code

https://claude.ai/code/session_015RMccximnhHjshZzajcbbf

[ahrazzle]

Review: math0 Lean results collection

Verdict: request changes. The audit design is good, and every check I could run came back clean. But CI doesn't do what the PR says: it replays cached results instead of re-checking the proofs. The statement freeze isn't enforced, and one result is now stale against OEIS. The PR is also too large to review as one unit.

What I checked, and what held up

• Audit commands (Audit.lean). #math0_proves / #math0_refutes compare types structurally against the upstream constant (mdata stripped, universe parameters compared). An axiom whitelist runs via collectAxioms. #math0_settles requires a universe-monomorphic def … : Prop that is itself sorry-free. This design is sound.
• Coverage. Math0.lean imports 131 result files, which contain exactly 131 audit commands (36 proves, 3 refutes, 4 refutes_every_answer, 88 settles), matching the 131 catalog entries.
  • Every settles targets Math0.Statements.<A>.statement, defined in the matching frozen file, and no proof file redefines it.
  • All 88 statement files are listed in FROZEN.sha256.
  • Every proves/refutes target is an upstream constant, and no Math0 declaration shadows one.
• Red flags. None found anywhere under lean/: no sorry, admit, native_decide, axiom, implemented_by/extern, debug.skipKernelTC or run_cmd/run_elab, and nothing redefines the #math0_* syntax.
• Generated files. Re-running scripts/gen_contents.py and scripts/gen_root.py leaves the tree unchanged.
• OEIS fidelity (sampled). I fetched all 88 frontier entries from oeis.org today and compared each quoted conjecture with the live text. 86 match closely; the other two are format differences, not errors.
  • I also read the entries where wording like "proof", "is true" or "holds" sits next to a conjecture that math0 lists as new (A073642, A086004, A092054, A127752, A249434, A333650, A363482, A369366, A393794). None of them already resolves the conjecture math0 claims.
  • The exception is A057566 (inline): OEIS corrected that formula on 21 Oct.
• Numbers. A083020: (3^(3^18) + 2) % 961 == 0 ✓. A393794: T(108910890) = 108910890, 9 digits, ≠ a 5 ✓.

Blocking

1. CI replays instead of rebuilding (inline on lean.yml). In the latest run every result module is Replayed from the Actions cache.

2. The freeze isn't enforced (inline). A statement and its hash can change together, and in this history they always land in the same commit as the proof.

3. A057566 refutes a formula that OEIS has since corrected (inline).

4. Size. 551 files, 104,833 lines, 56 commits, including 92 committed paper.pdf files (30 MB) alongside their .tex sources. The kernel checks the proofs, but statement fidelity needs a human, and nobody can do that across 88 statements in one PR. Suggest splitting it:

   • (a) infrastructure (Audit.lean, CI, lakefile, scripts, catalog schema) with its negative tests;
   • (b) the formal-conjectures track;
   • (c) frontier results in batches.

   Build the PDFs in CI or attach them to releases instead of committing them.

Should fix

5. README headline rule (inline). "Written by someone else" is true for 43 of 131 results.

6. "New result (open problem settled)" overstates some entries.

   • A073642's own result page says the identity "also follows from Gutkovskiy's 2019 g.f. in the entry".
   • A393794's counterexample 108910890 is 10 × 10891089, the "1089‖1089" concatenation, i.e. the non-primitive kind that the entry itself sets apart. The literal refutation is valid, but it reads more like an OEIS correction.

   Consider a more modest label (e.g. "OEIS conjecture settled") and keep "open problem" for results a referee judges non-routine.

7. PR description is stale. It says 86 manuscripts; the tree has 92.

8. Conflicts with other open PRs. README.md conflicts with #3 and #6, and .gitignore is add/add with #3. #6 describes math0 as a hub whose projects get their own repositories, which doesn't fit merging this collection into math0. The maintainers should decide math0's role first.

Minor: CI shows eight linter.unusedSectionVars warnings in A357216.lean (hn unused).

---

Generated by Claude Code

[ahrazzle]

The freeze check can't catch a statement edited together with its hash. sha256sum -c compares each statement with a hash file in the same tree, so a PR that edits a statement and updates FROZEN.sha256 passes. In this branch's history, statements, hashes and proofs always land in the same commit. Two statements were rewritten between their first appearance (97f6910) and their freeze, each in the same commit as its proof:

• A392943 in d151955;
• A394981 in 2ceb0fd, where it was re-encoded with padded cell indices.

I'm not suggesting anything wrong happened. But "fidelity-reviewed and frozen before any proof attempt" can't be confirmed from the repo. Cheap fixes:

• CODEOWNERS on lean/Math0/Statements/** (including FROZEN.sha256), requiring a human review;
• a pull_request CI step that fails if any existing line of FROZEN.sha256 differs from the base branch (adding lines stays allowed);
• land each statement in its own commit or PR, before the proof that uses it.

---

Generated by Claude Code

[abu-aska]

Two of the three fixes are in (0630a37). The third, CODEOWNERS, is open.

• scripts/check_freeze.py replaces the bare sha256sum -c.
  • Every frozen hash must still match its file.
  • FROZEN.sha256 is append-only against the base: no existing line may change or disappear.
  • Every math0-formalized statement in the catalogue must be listed.
  • On pull requests, each new result's statement must have been committed in a strict ancestor of the commit that adds its proof.
• Statements frozen before this check existed were committed together with their proofs, so git can't show their order. They are listed in FROZEN_WITH_PROOF.txt (94 entries), and their result pages now say so.
• From now on, statements land first, on their own. 7139d9f (4 statements) and 21c2fb4 (6) were pushed before any of their proofs succeeded. The order check will apply when those results land. lean/Math0/Statements.lean imports every frozen statement, so pending ones are compiled too.
• CODEOWNERS needs a maintainer to name the owners, so I've left it for them and this thread open.

---

Generated by Claude Code

[ahrazzle]

The current independent-kernel-replay run is incomplete: shard 1 has a failed job conclusion, its module-build step remains recorded as in progress, and its replay step never started. This is a runner/check-completion gap, not evidence of a rejected proof. The main Lean build and the other three replay shards passed. A completed successful replay of the missing shard is needed before merge.

The freeze hashes and generated catalogue checks pass locally for 137 results. The freeze-order command checks zero new results because the legacy exemptions cover this batch, so it does not independently establish their freeze-before-proof history. The earlier requests to review statement fidelity in bounded batches and resolve the collection versus hub placement remain open.

[abu-aska]

This covers both reviews (25 Oct and 28 Oct). The four inline threads have their own replies.

Done

• 1. CI replays the cache. Fixed: the build is now uncached, batched and checked against the catalogue count. On 21c2fb4 it passed in 53 min. Kernel replay (leanchecker in 4 shards, plus axiom-audit) also passed, except for shard 1. That runner died mid-build, before any replay. The new head 2580222 reruns all shards; I'll follow it until every shard has completed and passed.
• 2. Freeze. FROZEN.sha256 is now append-only, enforced by CI. New results get a freeze-before-proof order check, and 10 statements have since been committed ahead of their proofs. As the 28 Oct review notes, the check verifies 0 of the 137 current results: all 94 math0-formalized statements so far are in FROZEN_WITH_PROOF.txt. Their freeze order is attested only by the pipeline's logs, and their result pages say so. CODEOWNERS is for the maintainers to set.
• 3. A057566. Retitled, with a note about the 21 Oct correction. The corrected formula is a separate result, A057566b, frozen before its proof.
• 5. README rule. Reworded.
• 6. Labels. "New result (open problem settled)" now reads "New result (conjecture settled; no earlier resolution found)". An independent assessor judged each of the 61 new results, and a second assessor challenged every "substantial" verdict. 60 are routine and 1 is substantial (A278212). Routine here means a short or standard argument, something that follows from material already in the entry, or a finite search. Each result page gives the reasons, and the highlights and CONTENTS show the split.
  • A073642: routine. The page says it follows from Gutkovskiy's g.f. and from a one-line binary-increment step.
  • A393794: the assessor did not judge it literal-only. The entry's "primitive" remark describes a(n) itself, while the uniqueness claim covers all (n+4)-digit numbers. Still, the counterexample is 10 × 10891089, the non-primitive kind, and the assessment says the refutation needed no new idea.
• 7. PR description. Updated to match the tree.
• Minor: the eight unusedSectionVars warnings in A357216 are gone (omit hn in; the proof still checks).
• Negative tests: the audit tests weren't actually committed before, despite what the description said. They are now in tests/audit/ and run by CI: eleven files that must be rejected and one that must be accepted.

Left to the maintainers

• 4. Size and splitting, and the committed PDFs. I can split this into (a) infrastructure, (b) the formal-conjectures track and (c) frontier batches, or move the PDFs to CI or releases. I haven't, because both reshape the repository and that's the maintainers' call.
• 8. Collection or hub. Merging main conflicted on README.md. I kept main's hub README unchanged, apart from one row in its projects table pointing to RESULTS.md, which now holds this collection's page. Whether the collection stays here or moves to its own repository, as the hub README suggests for larger projects, is the open decision.
• Fidelity review in bounded batches. The 94 math0-formalized statements still need human review of fidelity. I can prepare batches, for example 10 statements per PR with each OEIS text beside its Lean statement, once the maintainers choose a structure.

---

Generated by Claude Code

[abu-aska]

Kernel replay on 2580222 completed in full (run 40875304335). All four leanchecker shards passed, shard 1 included (replay 13:34–13:51 UTC), and so did axiom-audit. Each job also rebuilt every module from scratch first.

Since then, the replay workflow no longer cancels a running replay when a new commit is pushed. Instead it queues one newer run behind it, so a replay always finishes.

---

Generated by Claude Code

[abu-aska]

On reviewing statement fidelity in bounded batches: review/fidelity/ (140e4ff) has eleven packets of ten statements, covering all 110 that math0 formalized itself. Each entry quotes the OEIS conjecture beside the frozen Lean statement. It also restates the Lean in plain words, says what the kernel checks against the OEIS data, and flags anything to look at.

An adversarial agent prepared them, so they are not a human review; they are meant to make one quick. That pass found no unfaithful or questionable statement and no major point. It flagged 15 minor points, all listed first in the index. They are:

• reading choices: offset shifts, n = 1 exclusions;
• data checks that run on a computable stand-in rather than the definition used in the statement;
• the "except for 9/49" wording of A362086 and A363482. Read strictly, each conjecture also needs that value to occur only once. That holds by computation for n < 1200 but is not part of the Lean result, and both result pages now say so.

The pass also found an OEIS data error, which I recomputed exactly: A386538's listed terms are wrong at n = 13, 17, 18, 22 and 23. The math0 counterexample at n = 7 is unaffected.

If the maintainers want fidelity reviewed in separate PRs, the packets can serve as the batches.

---

Generated by Claude Code