#!/usr/bin/env python3"""Finds candidate "problem solved with AI" items across several sources:   1. arXiv: papers in math / theory categories whose title or abstract smells     like a resolution (conjecture, counterexample, disproof, open problem,     ...), harvested over OAI-PMH - arXiv's own bulk interface, which does     date windows natively (no 12000-result cap, no deep-pagination 500s)     and is keyless. Daily runs resume from a checkpoint, so skipped days     are covered by the next run. For each candidate the HTML full text     (when arXiv has one) is fetched and searched for AI-model mentions -     that is where AI-use disclosures actually live, not in the abstract.     The search API remains only as a fallback when the harvester fails.  2. GitHub PRs: google-deepmind/formal-conjectures (any resolution-flavoured     or AI-mentioning PR) and leanprover-community/mathlib4 (AI-disclosing PRs     only - mathlib requires disclosure in the PR body, and every mathlib PR     is "proofy" so that filter alone would drown the report).  3. Tao's ledger: the AI-contributions wiki page on teorth/erdosproblems,     parsed by table and outcome. Only PRIMARY sections (AI doing the     mathematics) can be solves; solve-grade rows (green full solutions,     white candidates) print in detail with their source links, partial /     variant / incorrect rows get one-liners, and secondary rows     (literature search, formalizing human proofs) only a count.  4. Zenodo: recent records that look like a resolution and mention a model     (some authors publish there instead of arXiv - the SSUF papers did).  5. News feeds: OpenAI and DeepMind announcement RSS, the Kourovka Notebook     blog and the Xena project blog, filtered to math-resolution keywords.  6. An external aggregate claim index (URL supplied locally via the     FINDER_INDEX_URL env var or scripts/.finder_index_url, deliberately     not named in the repo). Claims whose links match nothing in our     catalog (arXiv id, Erdős number, GitHub repo, Zenodo id, vibemathed     slug) surface for triage - it aggregates far more than any single     upstream, so this is the broadest net.  7. Watched artifact repositories (plby/lean-proofs, Demonstrandum,     AlphaProof results, ten-proofs, ...): new commits in the window.  8. Trackers: Star Fleet Math's proposed-solution list (Erdős numbers),     Epoch AI's FrontierMath open-problems pages, and 1stproof.org's     batch/announcement links - new items only.  9. Registries: the Palomar registry's recent.json (new Lean developments     registered with a comparator-separated statement - the first two     Palomar-listed entries in the catalog both arrived as reader     submissions, which is how this source was found to be missing);     erdosproblems.com's forum index, read for proof-claim anchors, so a     claim filed on a problem page surfaces here the day it is filed rather     than when Tao's ledger next mentions it (the prime-gaps claim of     26 Aug 2026 was missed for four days that way); and watched GitLab     projects, which the GitHub-only repo watcher could not see (AI     Village's graffiti-verification, 197 claimed refutations). The first     run records a baseline and prints counts only; later runs print new     items. Zero dependencies (stdlib only). A state file remembers everything alreadyreported, so repeated runs only surface NEW finds. Every source fails soft:a dead endpoint prints a note and the rest of the report still runs. Usage:  python scripts/find_ai_solves.py                    # last 5 days, all sources  python scripts/find_ai_solves.py --days 7  python scripts/find_ai_solves.py --sources github,zenodo   # subset (arxiv,                                                     # github, erdos, zenodo, feeds)  python scripts/find_ai_solves.py --reset            # forget seen-state first  python scripts/find_ai_solves.py --since 2026-07-01 --until 2026-08-01                                                      # a fixed window (backfills);                                                      # same OAI harvest as daily                                                      # mode, any size, resumable Output is a Markdown report on stdout: triage it against the methodology(vibemathed.com/methodology) before anything becomes an entry.""" from __future__ import annotations import argparseimport jsonimport osimport reimport sysimport timeimport urllib.errorimport urllib.parseimport urllib.requestimport xml.etree.ElementTree as ETfrom concurrent.futures import ThreadPoolExecutorfrom datetime import datetime, timedelta, timezonefrom email.utils import parsedate_to_datetimefrom pathlib import Path from ratelimit import LIMITER # Windows consoles default to cp1252, which cannot print the math papers'# own characters. The report is UTF-8, unconditionally.sys.stdout.reconfigure(encoding="utf-8", errors="replace") STATE_FILE = Path(__file__).parent / ".find_ai_solves_state.json" # The models whose mention in a paper marks it as AI-assisted work.MODEL_TERMS = [    "Claude", "GPT", "ChatGPT", "Codex", "Gemini", "Grok",    "Aristotle", "AlphaProof", "AlphaEvolve", "LLM-assisted",    # Agents seen in the wild that are not model brands.    "Danus", "Rethlas", "AxiomProver",] # Generic phrasings, matched ONLY against a paper's own title and abstract.# In full text they are worthless: "Conference on Artificial Intelligence and# Statistics" is a venue, "large language models (LLMs)" is usually a citation,# and a 14-day sweep matching these anywhere returned 224 hits from 630 papers.# In an abstract, the same words are the authors describing their own method.GENERIC_TERMS = [    "generative AI", "language model", "AI system", "AI-assisted",    "AI-generated", "AI-guided", "artificial intelligence",    "automated theorem prov",]GENERIC_RE = re.compile("|".join(re.escape(t) for t in GENERIC_TERMS), re.IGNORECASE) # Contexts where a model mention means the opposite of a contribution. Writing# help is below our bottom tier, so a paper whose only AI mention is a language# -polishing declaration is not a candidate at all.NOISE_RE = re.compile(    r"improve the English|language editing|writing process|proofread|grammar"    # Found by triage 2026-08-03: an isoperimetric paper's only model mention    # was "used to help eliminate typos, mistakes and inconsistencies from the    # text", which is the same class as English-polishing.    r"|eliminate typos|inconsistencies from the text|copy-?edit"    r"|Conference on Artificial|Journal of Artificial|Cited by",    re.IGNORECASE,)  def _model_term(t: str) -> str:    """One model name, guarded against running into other words.     No LETTERS on either side: "GPTV01" and "GPTW24" are citation keys,    "grokking" is a phenomenon, "GPTs" is usually generalized probabilistic    theories - each of these cost a full-text fetch and a human look in the    May 2026 sweep. Digits stay allowed on purpose: "GPT4" and "Gemini 3    Thinking" are real names.    """    return rf"(?<![A-Za-z]){re.escape(t)}(?![A-Za-z])"  MODEL_RE = re.compile("|".join(_model_term(t) for t in MODEL_TERMS), re.IGNORECASE) # Contexts where a guarded term still is not a model. Each line is a real# false positive from a measured sweep, not a guess: "Aristotle University of# Thessaloniki" flagged an ergodic theory paper (2026-08-03); mathematics is# full of French Claudes (Berge, Chevalley, Shannon's first name, and the# Universite Claude Bernard in Lyon on half of all French affiliations); and# "[GPT23]" is an author-initials citation key, which the letter guard cannot# catch because a digit follows.## Applied per SNIPPET: a paper mentioning both Claude-the-model and Claude# Bernard still surfaces through the model snippet.MODEL_FALSE_POSITIVE_RE = re.compile(    r"Aristotle University|Aristotle's|Codex (?:Sinaiticus|Vaticanus)"    r"|Universit[ée]\w* Claude|Claude[- ]Bernard"    r"|Claude (?:Berge|Shannon|Chevalley|Laflamme|Gittelson|Bardos|LeBrun|Viterbo)"    r"|GPT[A-Z]{0,2}\d{2}(?!\d)",    re.IGNORECASE,) # What a resolution smells like, in a title or abstract.RESOLUTION_RE = re.compile(    r"conjecture|counterexample|disproo?f|disprov|open problem|open question"    r"|long-?standing|resolv|settles?|refut|first proof"    # "answers a question of X" is the commonest way a paper says it closed    # something, and its absence hid both Danus results in July 2026.    r"|answers? (?:a|the|this) question|answering (?:a|the) question"    r"|affirmative answer|negative answer|remained open|left open"    # Record ladders on a famous open problem never say "conjecture" or    # "resolve" - they say "improved lower bound". That gap hid the whole    # Shannon capacity chain (Gao 2607.27869, Buys-Polak-Zuiddam 2607.29681),    # even though the catalog already had an entry for the same ladder.    r"|improved? (?:lower|upper) bounds?|new (?:lower|upper) bounds?"    r"|better (?:lower|upper) bounds?|sharpens?|strengthens?"    r"|best (?:known|possible) bound|record",    re.IGNORECASE,) # Categories where model names are the SUBJECT, not a disclosure. A paper in# cs.LG about language models mentions "GPT" on every page, so the full-text# product arm matches it every time; these supplied all eight junk hits in the# measured sweeps. Excluded from the AI-mention test entirely, not from the# scan - a genuine resolution posted here would still need a math cross-list.ML_CATEGORIES = ("cs.LG", "cs.AI", "cs.CL", "cs.CV", "cs.NE", "cs.IR", "stat.ML") ARXIV_CATEGORIES = [    "math.CO", "math.NT", "math.AG", "math.PR", "math.GR", "math.CA",    "math.MG", "math.AC", "math.GT", "math.LO", "math.OC", "math.SP",    "math.DS", "math.AP", "math.RA", "math.RT", "math.FA", "math.ST",    "cs.CC", "cs.DM", "cs.DS", "cs.FL", "cs.LG", "quant-ph", "math-ph",] # PR sources. ai_only repos report ONLY PRs whose title or body mentions a# model - the volume filter for repos where every PR is about proofs.PR_REPOS = [    {"repo": "google-deepmind/formal-conjectures", "ai_only": False, "max_pages": 3},    {"repo": "leanprover-community/mathlib4", "ai_only": True, "max_pages": 10},] # Announcement feeds worth watching, filtered by RESOLUTION_RE. The Kourovka# blog posts solution announcements for the notebook's problems; Buzzard's# Xena blog covers formalization-adjacent AI mathematics.FEEDS = [    ("OpenAI news", "https://openai.com/news/rss.xml"),    ("DeepMind blog", "https://deepmind.google/blog/rss.xml"),    ("Kourovka Notebook", "https://kourovkanotebookorg.wordpress.com/feed/"),    ("Xena project", "https://xenaproject.wordpress.com/feed/"),] # Result-artifact repositories where labs and individuals drop proofs. A new# commit is a triage signal; the commit message usually names the problem.WATCHED_REPOS = [    "plby/lean-proofs",    "demonstrandum-research/artifacts",    "google-deepmind/alphaproof-nexus-results",    "google-deepmind/superhuman",    "openai/ten-proofs",    "pitmonticone/kourovka",    "octonion/mathematics",] # Registries (source 9). Palomar publishes its whole recent window as one JSON# document on a data host; the site itself is client-rendered and useless to# curl. erdosproblems.com has no claims feed, but its forum index links every# proof claim as an anchor on the problem's thread, which is enough to notice a# new one. GitLab projects expose a keyless activity Atom feed at <path>.atom.PALOMAR_RECENT_URL = "https://data.palomar-registry.org/recent.json"ERDOS_FORUM_URL = "https://www.erdosproblems.com/forum/"ERDOS_CLAIM_RE = re.compile(r'href="/forum/thread/(\d+)/proof-claims#proof-claim-(\d+)"')WATCHED_GITLAB_REPOS = [    "ai-village-agents/village/graffiti-verification",] STARFLEET_URL = "https://www.starfleetmath.com/"EPOCH_URL = "https://epoch.ai/frontiermath/open-problems"FIRSTPROOF_URLS = [    "https://1stproof.org/",    "https://1stproof.org/second-batch.html",] ERDOS_WIKI_URL = (    "https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems") UA = {"User-Agent": "vibemathed-finder/1.0 (rasmus.lindahl1996@gmail.com)"} DATASET_URL = "https://vibemathed.com/api/dataset"ARXIV_ID_RE = re.compile(r"arxiv\.org/(?:abs|html|pdf)/(\d{4}\.\d{4,5})", re.IGNORECASE)FC_PR_RE = re.compile(r"github\.com/google-deepmind/formal-conjectures/pull/(\d+)", re.IGNORECASE)MATHLIB_PR_RE = re.compile(r"github\.com/leanprover-community/mathlib4/pull/(\d+)", re.IGNORECASE)ZENODO_ID_RE = re.compile(r"zenodo\.org/records?/(\d+)", re.IGNORECASE)ERDOS_NUM_RE = re.compile(r"erdosproblems\.com/(\d+)", re.IGNORECASE)GH_REPO_RE = re.compile(r"github\.com/([\w.-]+/[\w.-]+)", re.IGNORECASE)VIBEMATHED_RE = re.compile(r"vibemathed\.com/problem/([\w-]+)", re.IGNORECASE)  def _pacing_note(host: str, code: int, wait: float, attempt: int, why: str) -> None:    """Backoffs go to stderr, so the Markdown report on stdout stays clean."""    label = f"HTTP {code}" if code else why    print(f"  [pace] {host}: {label}, waiting {wait:.1f}s ({why}, attempt {attempt + 1})",          file=sys.stderr, flush=True)  def fetch(url: str, timeout: int = 30) -> str:    """Rate-limit-aware GET. Pacing is adaptive and shared per host - see    scripts/ratelimit.py for why a fixed sleep was the wrong shape.     A GITHUB_TOKEN env var, if present, authenticates API calls (5000/hour    instead of 60). Optional by design: every source works keyless.    """    headers = dict(UA)    if urllib.parse.urlsplit(url).netloc == "api.github.com":        token = os.environ.get("GITHUB_TOKEN", "").strip()        if token:            headers["Authorization"] = f"Bearer {token}"    return LIMITER.fetch(url, headers, timeout=timeout, on_wait=_pacing_note).decode(        "utf-8", errors="replace")  def load_state() -> dict:    state = json.loads(STATE_FILE.read_text()) if STATE_FILE.exists() else {}    # Older state files predate the newer sources; default every key.    state.setdefault("seen_arxiv", [])    state.setdefault("seen_prs", [])  # formal-conjectures numbers (legacy key)    state.setdefault("seen_mathlib_prs", [])    state.setdefault("seen_erdos_rows", [])    state.setdefault("seen_zenodo", [])    state.setdefault("seen_feed_items", [])    state.setdefault("seen_index", [])    state.setdefault("seen_repo_commits", [])    state.setdefault("seen_tracker_items", [])    # Registries keep a baseline flag as well as a seen-list: the erdosproblems    # forum index carries every proof claim ever filed, and printing all of    # them on the first run would bury the report. The first run records them    # and prints a count; only later runs print items.    state.setdefault("seen_registry_items", [])    state.setdefault("registry_baselined", False)    # Last date the default (non --since) arXiv harvest completed through.    # A run after a gap resumes from here instead of losing the gap days.    state.setdefault("arxiv_oai_until", "")    return state  def save_state(state: dict) -> None:    STATE_FILE.write_text(json.dumps(state, indent=1))  def context_lines(text: str, pattern: re.Pattern, limit: int = 3) -> list[str]:    """Short context snippets around each distinct match, for the report."""    out, seen_terms = [], set()    for m in pattern.finditer(text):        term = m.group(0).lower()        if term in seen_terms:            continue        seen_terms.add(term)        start, end = max(0, m.start() - 80), min(len(text), m.end() + 80)        snippet = re.sub(r"\s+", " ", text[start:end]).strip()        out.append(f"…{snippet}…")        if len(out) >= limit:            break    return out  def strip_tags(html: str) -> str:    return re.sub(r"\s+", " ", re.sub(r"<[^>]+>", " ", html))  # -------------------------------------------------------------- catalog ---- def catalog_index() -> dict:    """Ids already in the live catalog, per source kind.     Pulled from the site's own public dataset endpoint (sourceUrl plus every    extra link per entry), so finds that are already tracked get marked in the    report instead of wasting triage time. Fails soft: if the site is    unreachable, nothing gets marked and the report still prints.    """    known = {"arxiv": set(), "fc_prs": set(), "mathlib_prs": set(),             "zenodo": set(), "erdos": set(), "gh": set(), "slugs": set()}    try:        data = json.loads(fetch(DATASET_URL))    except Exception as e:        print(f"_(catalog check skipped: {e})_\n", file=sys.stderr)        return known    for p in data.get("problems", []):        known["slugs"].add(p.get("slug") or "")        # The problemNumber FIELD, not the slug: famous Erdős problems live        # under named slugs (erdos-planar-unit-distance is #90), so slug        # parsing alone under-counts what the catalog already tracks.        if p.get("problemNumber") is not None:            known["erdos"].add(int(p["problemNumber"]))        urls = [p.get("sourceUrl") or "", p.get("citationsUrl") or ""]        urls += [link.get("url") or "" for link in p.get("links", [])]        for u in urls:            for m in ARXIV_ID_RE.finditer(u):                known["arxiv"].add(m.group(1))            for m in FC_PR_RE.finditer(u):                known["fc_prs"].add(int(m.group(1)))            for m in MATHLIB_PR_RE.finditer(u):                known["mathlib_prs"].add(int(m.group(1)))            for m in ZENODO_ID_RE.finditer(u):                known["zenodo"].add(int(m.group(1)))            for m in GH_REPO_RE.finditer(u):                known["gh"].add(m.group(1).lower())    return known  # ---------------------------------------------------------------- arXiv ---- # The OAI-PMH harvester: arXiv's own bulk interface, and the primary way this# script reads arXiv now. Keyless, date-ranged, resumption-token paginated,# ~1000 records per response - none of the search API's failure modes (the# 12000-result cap, deep-pagination 500s, the sort-order dependence) exist# here, because bulk harvesting is what OAI-PMH is FOR.OAI_URL = "https://oaipmh.arxiv.org/oai"# The sets covering ARXIV_CATEGORIES. OAI serves whole sets; the category# filter runs client-side on each record's own category list.OAI_SETS = ["math", "cs", "physics:math-ph", "physics:quant-ph"]OAI_NS = {"oai": "http://www.openarchives.org/OAI/2.0/",          "ax": "http://arxiv.org/OAI/arXiv/"}CATEGORY_SET = set(ARXIV_CATEGORIES)  def arxiv_oai_window(from_date: str, until_date: str | None) -> list[dict]:    """Resolution-flavoured papers with a created date in the window.     Harvests by DATESTAMP (last metadata change), which is the only range    OAI-PMH offers. A new paper's datestamp is its announcement day, but its    `created` is the SUBMISSION day, typically days earlier - so the created    filter takes slack before the window rather than aligning with it, or a    one-day harvest would drop every new paper it returned (measured: 860    in-category records on 2026-08-04, zero with created that same day).    What the slack exists to exclude is the other kind of record a datestamp    harvest returns: v2s and metadata edits of years-old papers. Overlap    between adjacent sweeps is the seen-state's problem, and it handles it.    Dates are YYYY-MM-DD, both ends inclusive, in arXiv's clock (UTC).    """    slack = (datetime.fromisoformat(from_date) - timedelta(days=14)).date().isoformat()    papers: list[dict] = []    for oai_set in OAI_SETS:        token: str | None = None        pages = 0        while True:            if token:                query = f"verb=ListRecords&resumptionToken={urllib.parse.quote(token)}"            else:                query = (f"verb=ListRecords&metadataPrefix=arXiv&set={oai_set}"                         f"&from={from_date}"                         + (f"&until={until_date}" if until_date else ""))            root = ET.fromstring(fetch(f"{OAI_URL}?{query}", timeout=90))            err = root.find("oai:error", OAI_NS)            if err is not None:                # An empty window is an answer, not a failure.                if err.get("code") == "noRecordsMatch":                    break                raise RuntimeError(f"OAI {err.get('code')}: {(err.text or '').strip()}")            for rec in root.findall(".//oai:record", OAI_NS):                meta = rec.find(".//ax:arXiv", OAI_NS)                if meta is None:                    continue  # deleted/withdrawn record: header only                cats = (meta.findtext("ax:categories", "", OAI_NS) or "").split()                if not CATEGORY_SET.intersection(cats):                    continue                created = meta.findtext("ax:created", "", OAI_NS)                if created < slack or (until_date and created > until_date):                    continue                title = re.sub(r"\s+", " ", meta.findtext("ax:title", "", OAI_NS)).strip()                abstract = re.sub(r"\s+", " ", meta.findtext("ax:abstract", "", OAI_NS)).strip()                if RESOLUTION_RE.search(title + " " + abstract):                    papers.append({                        "id": meta.findtext("ax:id", "", OAI_NS),                        "title": title, "abstract": abstract,                        "primary": cats[0] if cats else "",                    })            pages += 1            tok = root.find(".//oai:resumptionToken", OAI_NS)            token = (tok.text or "").strip() if tok is not None else ""            print(f"  [oai:{oai_set}] page {pages}, {len(papers)} flagged so far",                  file=sys.stderr, flush=True)            if not token:                break    # Cross-listed papers arrive once per set they belong to (math.CO + cs.DM    # shows up in both harvests); one report each.    seen_ids: set[str] = set()    unique = []    for p in papers:        if p["id"] in seen_ids:            continue        seen_ids.add(p["id"])        unique.append(p)    return unique  def arxiv_recent(days: int, since: str | None = None, until: str | None = None) -> list[dict]:    """FALLBACK: the search-API scan, used only when the OAI harvest fails.     Papers in the target categories, resolution-flavoured only.     Default mode pages backwards from now. That cannot reach past roughly a    month: the result cap below is an absolute 12000, and these categories    produce enough submissions to exhaust it in about that time, so an older    window was simply unreachable no matter what --days said.     Passing --since/--until instead puts a submittedDate range into the query    itself, so the whole result set is the window and pagination starts at its    newest edge. That is what makes historical sweeps possible.    """    cat_query = "+OR+".join(f"cat:{c}" for c in ARXIV_CATEGORIES)    if since:        cutoff = datetime.fromisoformat(since).replace(tzinfo=timezone.utc)        hi = until or datetime.now(timezone.utc).strftime("%Y-%m-%d")        # Parentheses round the category OR group, or the AND binds to the        # last category only and the window silently does nothing.        window = (f"%28{cat_query}%29+AND+submittedDate:"                  f"%5B{cutoff.strftime('%Y%m%d')}0000+TO+{hi.replace('-', '')}0000%5D")    else:        cutoff = datetime.now(timezone.utc) - timedelta(days=days)        window = cat_query    papers, start, page = [], 0, 200    ns = {"a": "http://www.w3.org/2005/Atom"}    # Hard stop scaled to the window: ~1500 submissions/day across these    # categories, capped so a giant window cannot page forever.    #    # Scale it to the window actually being queried. With --since/--until the    # span is the date range, NOT --days, whose default of 5 would cap a    # three-week sweep at 7500 entries: paging would stop a third of the way    # in, silently, having covered only the newest end. That is the same    # silent-truncation failure as the swallowed paging error, arriving by a    # different route.    span_days = max(1, (datetime.fromisoformat(hi).replace(tzinfo=timezone.utc)                        - cutoff).days) if since else days    hard_stop = min(12000, 1500 * span_days)    while start < hard_stop:        url = (            "http://export.arxiv.org/api/query?search_query=" + window            + f"&sortBy=submittedDate&sortOrder=descending&start={start}&max_results={page}"        )        # arXiv 500s intermittently on deep pagination. Letting that propagate        # discarded the entire scan and printed "0 papers scanned", which reads        # as "nothing to find" rather than "the search broke" - the worst

Lines 1–500 of 1403. Load more