Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Verification records for L17
clean_gate/: The non-author clean gate of 2026-10-08 for L17: the committed Lean gate in clean mode over a fresh archive of the whole lean/ tree as it stood on 2026-10-08T13:58:11Z, exit 0, AUDIT PASS over 1 claim with 0 compiler axioms and the committed self-test stamp matched; the receipt, the captured log and the wrapper.
statement_fidelity/: The fidelity review, distinct grade, non-author clean gate, native binding and acceptance warrant for the first acceptance of L17, for the sources as they stood on 2026-09-25T03:40:15Z; the acceptance is kernel-only.
statement_fidelity_2/: The second independent statement-fidelity cycle of 2026-10-02 for L17: the blind review of Erdos.L17.statement against the frozen English statement, verdict refutation-failed, its distinct grade, pass with tier 2 asserted, kernel-only, bound to the lean/ tree the non-author clean gate of 2026-09-29 checked, and the reviewer's census scripts.
The current record holds the second-cycle
independent whole-statement fidelity review of 2026-10-02, verdict
refutation-failed, the distinct grade that asserts tier 2 for L17,
kernel-only with zero compiler axioms, bound to the lean/ tree the
non-author clean gate of 2026-09-29 checked and cited there, and the
reviewer's census scripts; the assertion is in force from the filing that
cites the grade and the gate together. The
clean gate of 2026-10-08 holds the non-author
runner's receipt, captured log and wrapper for the whole lean/ tree as it
stood on 2026-10-08T13:58:11Z (exit 0, AUDIT PASS over 1 claim with 0
compiler axioms, the self-test stamp matched), the gate the card's standing
cites with that grade; the claim's statement is unchanged in meaning from
the tree the grade examined to that tree. The
earlier record holds the first acceptance of
2026-09-25: its fidelity review, distinct grade, non-author clean-gate
receipt with its log and wrapper, the
native binding with the English
subject's extraction rule, and the
acceptance warrant, for a
branch tree as it stood on 2026-09-25T03:40:15Z, which the default branch
never carried; it is retained as an assessment of that subject, its
extension rule reaches no later tree, and no delivery confirmation was filed
under it.