Lean-verified proof of Robert Israel's OEIS A057923 two-step monotonicity conjecture, a(n+2) > a(n), for Larry Reeves' greedy bitwise-OR sequence. No novelty claim.
-
Updated
Oct 27, 2026 - Python
Lean-verified proof of Robert Israel's OEIS A057923 two-step monotonicity conjecture, a(n+2) > a(n), for Larry Reeves' greedy bitwise-OR sequence. No novelty claim.
Track record of NAI (No-Ansatz Inference), which finds formulas in data without a language model: benchmark results against other systems (SRBench, SLDBench, OEIS), accepted OEIS edits, proofs and preprints.
New terms a(10)–a(400) of OEIS A072503 (shoe lacings with no horizontal connections), computed with Claude Code. Two independent exact methods agree for n = 3..400.
The whole OEIS on your disk: offline, exact, millisecond integer-sequence lookup.
A logic kernel for reasoning about stability, collapse, and rhythm in bounded systems.
Independent verification for ten new terms of five OEIS bishop-graph sequences: format, structural identities, and a live check against the published record.
Find OEIS sequences that stopped early because a brute force ran out of patience, then extend them. Every extension reproduces all published terms first.
The least n with rad(n) | f(n) whose covering digraph has girth k, for eleven arithmetic functions and k = 2..10: 52 values proved minimal, 38 of them computed here for the first time, with a surgery theorem on the cycle and a certificate deciding m_f(k+1) < m_f(k) without computing it.
Full-database sweep of the OEIS for exact identities the encyclopedia doesn't record: 597,928 unrecorded pairs, 0% measured false-discovery rate, 592 b-file re-derivations with 0 divergences.
Lean 4 proof that n·exp(x·G^M(n))) satisfies b(n+k) ≡ b(n) mod k for shift-stable exponents. Resolves conjectures of Peter Bala on OEIS A361036, A361281, A293013, A278070.
Deterministic modular analysis toolkit for integer datasets and structural fingerprints.
Property definitions and the stateless compute engine (atlas-algos) for Integer Atlas — number-theoretic properties of the integers.
Work orders and accepted shard manifests for Integer Atlas — a pointer registry; data files live in object storage.
Transform-aware identifier for OEIS integer sequences
Validate OEIS entries against the internal format specification and style sheet
Collatz‑3: A Modular Variant of the Collatz Process
Experiments on the integer sequence A359012
Code for my contributions to the OEIS.
LODA Runtime and Machine Learning in Python
Some utilities for integers, integer sequences, arithmetic properties of integers, special sequences and sets
To associate your repository with the integer-sequences topic, visit your repo's landing page and select "manage topics."