A polished, reproducible generator for a local snapshot of every problem on ErdosProblems.com.

This public repository intentionally ships the generator—not the generated problem text. A run discovers the current collection, downloads each public LaTeX view, combines it with structured community metadata and the frozen AI contributions wiki, validates the result, and records content hashes and source revisions.

The collection changes frequently, and ErdosProblems.com does not publish an explicit full-text redistribution license. Generated statements, descriptions, references, metadata, source mirrors, and HTTP caches are therefore local and Git-ignored. This keeps the public repository current, useful, and conservative about third-party rights.

• Discovers the current problem count independently from the live homepage.
• Downloads every /latex/<id> page with retries, rate limiting, and a descriptive user agent.
• Fetches normal problem pages efficiently through public range views.
• Extracts four LaTeX fragments per problem:
  • statement.tex
  • description.tex
  • references.tex
  • combined problem.tex
• Produces rich per-problem JSON with:
  • open/resolved status and source conflicts;
  • prizes, tags, citations, OEIS links, and related problems;
  • Lean statement/formalization links;
  • human-resolution evidence from source descriptions;
  • normalized AI contributions and conservative provenance labels;
  • source URLs, Git revisions, retrieval times, and SHA-256 hashes.
• Writes searchable CSV and JSONL indexes.
• Supports fresh online generation and deterministic offline rebuilding.
• Includes a colorful progress UI, quiet/silent mode, and JSON output for scripts and CI.
• Validates all files, indexes, aggregate counts, AI table rows, status semantics, LaTeX hazards, and content hashes.
• Includes a simple static browser under frontend/ that builds directly from the generated JSONL and summary files.

Requirements: Python 3.11+ and Git.

git clone https://github.com/Yeyito777/leandosproblems.git
cd leandosproblems

python -m venv .venv
. .venv/bin/activate
pip install -r requirements.lock.txt

make sync
make validate
make stats

A fresh full run currently takes roughly a few minutes. The default global request-start interval is 0.15 seconds and can be made slower if requested by the source operator.

./generate.py [options]

  --workers N                 concurrent LaTeX workers (default: 4)
  --request-interval SECONDS  global delay between HTTP request starts
  --batch-size N              IDs per normal range page
  --offline                   rebuild from verified local caches
  --community-revision SHA    pin the community database commit
  --wiki-revision SHA         pin the AI wiki commit
  --limit N                   generate the first N problems for development
  -q, --quiet, --silent       suppress routine output
  --json                      output only compact summary JSON
  --no-color                  disable ANSI colors
  --debug                     show full tracebacks
  --version                   print the generator version

Interactive generation with progress bars:

./generate.py

Silent generation:

./generate.py --silent

Machine-readable/CI generation:

./generate.py --json | jq

Faster local concurrency while keeping the same global request rate:

./generate.py --workers 8 --request-interval 0.15

Deterministic rebuild with no network access:

./generate.py --offline

Pinned upstream revisions:

./generate.py \
  --community-revision <commit-sha> \
  --wiki-revision <commit-sha>

Small development run:

./generate.py --limit 10

A limited run intentionally replaces the local generated output with that subset. Run a full sync afterward to restore the complete local snapshot.

All paths below are generated and ignored by Git:

data/
├── summary.json
├── index.csv
├── index.jsonl
├── ai-contributions.json
└── problems/
    ├── 0001/
    │   ├── statement.tex
    │   ├── description.tex
    │   ├── references.tex
    │   ├── problem.tex
    │   └── metadata.json
    └── ...

sources/
├── community-database/
├── ai-wiki/
└── erdosproblems.com/robots.txt

snapshot.json
.cache/                 # raw HTTP and shallow Git caches

Every indexed problem has a nonempty statement.tex. Description and reference files may be empty when the source page has no corresponding section. The LaTeX files are fragments rather than universally standalone documents; the extractor normalizes the site's list templates, formatting spans, alignments, and unsafe literal # characters.

The practical record shape is documented in the generator and formalized in schema/problem.schema.json.

The generator treats these as unresolved/open:

• OPEN
• FALSIFIABLE
• VERIFIABLE
• DECIDABLE
• NOT PROVABLE
• NOT DISPROVABLE
• INDEPENDENT

It treats PROVED, DISPROVED, and SOLVED as resolved. Both the visible per-problem status and the site's raw technical open/solved DOM bucket are retained because those two representations occasionally disagree.

A “formalized statement” means that the conjecture has been encoded in Lean. It does not by itself mean that a proof or disproof has been formalized.

There is no trustworthy universal binary “human or AI” field, so the generator does not guess. It preserves:

• source paragraphs that discuss proofs and solvers;
• all relevant rows from the frozen AI contributions wiki;
• indicator sets for full, partial, incorrect, mixed, and unverified outcomes;
• whether a primary green event explicitly claims a full problem resolution;
• whether the recorded work was AI-standalone, alongside literature, building on literature, or a significant human–AI collaboration.

Absence of a recorded AI event is not labeled “human-only.” Wiki records are provisional, selection-biased, frozen as of June 30, 2026, and are not independent verification of the mathematics.

Each HTTP cache entry has a sidecar containing its URL, actual retrieval time, HTTP metadata, byte length, and SHA-256. snapshot.json records every response, all generated-file hashes, upstream Git revisions, and the generator revision. Offline rebuilds preserve source retrieval times and produce deterministic outputs.

Validate a full snapshot with:

python scripts/validate.py

Print a concise report with:

python scripts/stats.py

Build and serve the generated browser locally:

make frontend
make frontend-serve

Then open http://localhost:8080. The frontend is contained explicitly under frontend/, uses no JavaScript framework, and reads a compact Git-ignored bundle produced from data/index.jsonl and data/summary.json. It supports metadata search, independent official-status, reported-AI-result, and subject-tag filters, pagination, source and formalization links, OEIS links, and conservative aggregate AI provenance. The AI filters distinguish reported human–AI full solutions, primary partial AI results, and reported full solutions with no significant human involvement recorded. They do not override the official ErdosProblems.com status. The public bundle intentionally excludes full statements, descriptions, references, and normalized AI-wiki rows.

The software in this repository is MIT licensed. That license does not relicense generated third-party material.

• The community database at teorth/erdosproblems is Apache-2.0 licensed; its license and citation metadata are copied into the generated sources/ tree.
• ErdosProblems.com allows general crawling in the captured robots.txt, but crawling permission is not a full-text redistribution license.
• No separate redistribution license was identified for the copied AI wiki.

Do not commit or publish generated full-text output without permission or another valid legal basis. See THIRD_PARTY_NOTICES.md for the conservative publication boundary.

Generator code and repository documentation: MIT.

Generated third-party content retains the rights and licenses applicable at its sources.