Plectis Mathematics
Expand the mathematics map Expand the system map

Eight Erdős problem programmes

Each page gives the original question, the results checked in the Lean proof assistant, the approaches that failed and what remains unproved.

  1. #68The factorial-denominator seriesOpen
  2. #243Reciprocal-tail rigidity near the Sylvester recurrenceOpen
  3. #249The binary totient seriesOpen
  4. #251The prime-gap dyadic seriesOpen
  5. #257Reciprocal sums over infinite exponent supportsOpen
  6. #269Three-prime running least common multiplesOpen
  7. #1041Short connections inside polynomial lemniscatesFormal statement refuted
  8. #1049Lambert-type series at rational basesOpen

“Open” means the Erdős problem itself is unsolved. “Formal statement refuted” means Lean disproves the exact Formal Conjectures statement; whether it matches the historical wording needs separate human review.

Each dot is a result stated in one of the papers; red ones have a Lean proof re-checked by a separate program.

Lean source

Eighty-eight software components

The earlier Plectis software: 88 components from my research system, in seven families.

  1. Entry & orientation2
  2. Architecture & navigation12
  3. Formal math & proof20
  4. Agent reliability & safety20
  5. Research & science9
  6. Import & drift control20
  7. Work & continuity5

The map of the system draws here when its script runs. The list beside it gives the same families as text, and the full map opens every component.

Papers

All 22 papers, with abstracts and sources →

Each problem has a short paper, which contains the compressed ideas, and a long paper, which is a reasoning record of all the failed routes and attempted avenues. The three below are good places to start.

  1. Research paper, 26 pages Irrationality criteria for Lambert subseries

  2. Companion, 6 pages Plectis: Verifying Code and Recording Its Execution

These author-released papers are not externally peer reviewed and have no DOI. Lean checks statements; readers judge novelty and significance.