The system
The papers
Published PDF papers, grouped by the question each one answers. Every covered Erdős problem has its own paper; Problems #249 and #257 also have full reasoning papers. Pending and retired manuscripts are labelled separately.
A paper explains the work. Proof validity belongs to the Lean source checked by the pinned kernel, and public claim status belongs to the claim registry that records it. Where a paper and a source disagree, the source wins. Each published entry links the LaTeX the hosted PDF was built from. The component documentation is a separate technical-note corpus and is indexed under Components.
The mathematics
What is proved for each covered open Erdős problem, and what still blocks it?
Integral Channels and the Prime Unit Translator
What exact denominator obstructions are checked for Erdős #68, and which quantified producer could still prove irrationality?
For the factorial-denominator series, Lean gives an exact factorial-successor normal form and the equivalent eventual-unit-carry criterion, together with integral-channel, prime-translator, projection-rigidity, and Cramer-residual consumers. An independently regenerated exact finite certificate reaches index 300000, and the checked consumer excludes every smaller positive rational denominator. Five quantified producer problems isolate the missing cofinal step; none is proved, and Erdős #68 remains open.
- Explains
- the problem-specific exposition for Erdős #68: exact factorial normal forms, structural consumers, finite denominator evidence, method boundaries, and five ranked open producers.
- Not authority for
- proof validity, which belongs to Lean source checked by the pinned kernel, or a solution to Erdős #68, which remains open.
- Where to start
- problem, channels, projection, open (our selection, not the paper's own advice)
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
Excluding the Bounded Negative Part
Which bounded negative-error behaviours can be excluded for Erdős #243, and which analytic hypotheses still keep it open?
Clearing denominators turns Erdős #243 into rigidity of a centred integer error orbit. Lean excludes eventually negative constant magnitude and positive-drift periodic magnitude, and proves that normalised vanishing plus an eventually bounded negative part forces the error to vanish and the Sylvester recurrence to begin. Eventual strict centring is redundant, while Koizumi supplies normalised vanishing for the canonical orbit. The missing hypothesis is the negative-part bound: any survivor has cofinally unbounded negative excursions and divergent normalised negative mass.
- Explains
- the problem-specific exposition for Erdős #243: the centred integer state, negative-part exclusions, conditional theorem, and remaining analytic obligations.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
A Basis for the 2-Kernel of Euler's Totient
What is proved about the dyadic sections of Euler's totient and the finite denominator bound, and what still blocks Erdős #249?
The dyadic sections of Euler's totient have an explicit rational basis: the true truncation has dimension 1 at level 0 and exactly 2^e + 1 for e at least 1, so the full span is infinite-dimensional. A 240-bit Farey window excludes every reduced denominator through 79,639,646,646,701,375,323,355,774,875,831,053, and exact diagonal certificates exist for every t through 82. No t = 83 certificate, cofinal supply, or matching rank upper bound is proved; Erdős #249 remains open.
- Explains
- problem-specific mathematical exposition for Erdős #249: the exact finite-level rank, infinite-dimensionality consequence, denominator exclusion, method limits, and open edge.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
The Binary Totient Series
What has been tried on Erdős #249, which routes are closed, and what exact cofinal obligations remain?
A claim-bounded map of the formal attack on Erdős #249. It front-loads the exact totient-kernel basis and level rank, the approximately 7.96 x 10^34 denominator exclusion, and diagonal certificates for every t through 82, then records the hypotheses, source sites, coordinate-specific obstructions, and open interfaces. The cofinal certificate and tail-nonintegrality statements are exact reformulations, not a solution: no t = 83 or unbounded producer is obtained, and Erdős #249 remains open.
- Explains
- a claim-bounded problem-specific reasoning surface for Erdős #249: selected checked premises, finite certificates, closed routes, surviving obligations, and their exact evidence bands.
- Not authority for
- proof validity, which belongs to Lean source checked by the pinned kernel, or a solution to Erdős #249, which remains open.
- Where to start
- wall, survivors (our selection, not the paper's own advice)
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
An Integral-Shift Criterion for Dyadic Tail Recurrences
What tail-shift condition would prove irrationality in Erdős #251, and what prime-gap input is still missing?
For any sequence obeying the dyadic recurrence with integer digits, a shift of length h is an integer exactly when one explicit multiple of the term is, and integrality then propagates to every later index; over the reals the contrapositive is an irrationality criterion. Applied to the prime-gap series — conditional on a summability input the prime number theorem supplies but which is not formalised here — this makes the remaining obligation exact: cofinal non-integrality for every fixed h. Erdős #251 stays open.
- Explains
- the problem-specific exposition for Erdős #251: summation by parts, dyadic tail recurrences, integral-shift criteria, local certificates, and the remaining cofinal condition.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
Denominator Periods, Rational-Value Constraints and Achievement-Set Geometry
Which Mersenne-support subseries are settled, what finite-period and achievement-set structure is proved, and what still blocks Erdős #257?
For every finite support and integer base, the reduced denominator has multiplicative order exactly the support lcm. Restricted achievement sets also receive exact coding, topology, perfectness, and measure statements with their finite/infinite hypotheses. Rational infinite supports must satisfy explicit long-division and divisor-incidence constraints, but those constraints do not conflict. Prime support at base 2 and squarefree support at power-of-two bases are cited prior results, not contributions here. The targets 1/2 and 1/21 reduce to open infinite-orbit alternatives; Erdős #257 remains open.
- Explains
- problem-specific mathematical exposition for Erdős #257: exact finite periods, settled support families, method limits, and the open half-value edge.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
Reciprocal Mersenne Subseries
What has been tried on Erdős #257, which routes are closed, and what exact universal and half-value obligations remain?
A Lean-backed, claim-bounded structural audit of Erdős #257. It front-loads finite-denominator noncollapse; exact restricted-set coding, topology, perfectness, and measure; a squarefree-support method boundary; and an exact carry-pivot normal form. Prime support at base 2 and squarefree support at power-of-two bases are identified as cited prior results. The targets 1/2 and 1/21 have no finite-support representation and reduce to explicit infinite-orbit alternatives. Neither target membership nor universal #257 is decided.
- Explains
- a claim-bounded problem-specific reasoning surface for Erdős #257: selected checked premises, finite computations, closed routes, surviving obligations, and their exact evidence bands.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
The Three-Prime Running Least Common Multiple
What exact running-LCM structure is proved for Erdős #269, and which residue-escape conditions remain unproved?
For three primes, Lean gives the exact running-lcm product, logarithmic cells, shell bounds, the four-value block radix at 2, 3, 5, and a rank-two nonseparability witness; these are the note's unconditional contributions. For every pair of distinct primes, both the de-duplicated sum and Erdős's repeated running-lcm sum are transcendental by a paper argument that is not Lean-formalised, over the Loxton--van der Poorten 1977 engine quoted in Bugeaud--Laurent form; Steve Fan posted the same reduction and conclusion on the problem's public discussion page on 26 June 2026, and the note claims no priority for it. The remaining criterion is conditional: its rationality-to-carry divisibility bridge and cofinal residue escape are unproved, while the reported scan is finite. Erdős #269 remains open from three primes onward.
- Explains
- the problem-specific exposition for Erdős #269: the two-prime analytic deductions, three-prime product formula, cell and shell structure, non-separability, finite experiments, and remaining cofinal escape condition.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
Newton Flow and Critical-Value Ray Separation
Which Newton-flow separation facts are checked for Erdős #1041, and what exactly fails in the recent claimed global decomposition?
Along the complex Newton field, Lean checks that the polynomial value decays as exp(-t) and therefore stays on one oriented ray. It formalises the resulting no-connection criterion, the exact translation ray-collision locus, finite-line avoidance, and a root-retention bound. A recent manuscript's load-bearing Proposition 12 uses an invalid three-ended local block at an interior Morse saddle; the proposition is not refuted and may admit a four-pronged or cut-annulus repair. The global topology and length gluing remain open.
- Explains
- the problem-specific exposition for Erdős #1041: Newton-flow ray separation, perturbation inputs, the exact printed proof gap, and the ranked topology and metric repair questions.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
Multiplicative Obstructions at Base 3/2
Which linear-form constructions fail at the rational base 3/2 for Erdős #1049, and what primitive kernel is still needed?
At the resistant base 3/2, Lean rules out two common-width linear-form mechanisms: scalar content gives no net local-to-Archimedean gain, and unit endpoints exclude both 3 and 2 from a common divisor. A four-jet count constructs a signed relation but not a nonzero analytic remainder; direct cut-level clearing also incurs an exponential denominator factor and an impossible corridor inequality. The elementary 7/2 height bound is formalised, but the published analytic criterion remains external. These are construction-specific exclusions, not an irrationality result; Erdős #1049 remains open.
- Explains
- the problem-specific exposition for Erdős #1049: content and endpoint obstructions, the failed coordinatewise-clearing route, height arithmetic, and the remaining primitive construction.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
The publication method
A machine checked the proof — but who checks that the public wording describes it faithfully?
From Lean Proofs to Public Claims
Lean proves the formal statement — but who checks that the README describes it faithfully?
Lean checks that a proof establishes the formal statement written in the source. It does not check that a README or paper describes that statement faithfully. For each selected result a mathematician records the public wording, the formal statement said to support it, the range actually proved, and the adjacent stronger statement that remains open; the release workflow then checks that later edits preserve those relationships. A historical README edit that erased the finite-versus-open distinction passed because the relationship had not been registered; after registration, a deliberately false copy was rejected. That is one failure and one repair, not complete claim discovery.
- Not authority for
- the mathematical content it uses as its worked example, and the correctness of the human review it preserves.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
From a Cold Clone to a Proof Receipt
How can a reasoning agent comprehend a large Lean corpus before compiling, then cross into replayable proof authority and incremental validation?
A large formal library can be mechanically exact and still be practically unreadable to the next reader or reasoning agent. At the audited revision a cold clone exposes a bounded six-line tour over 1,019 Lean modules and 153,238 declarations, a map of ten programmes, 101 curated claims, and an elaborated reference graph — none of which requires a build; 503 of those modules and 8,171 of those declarations are machine-generated certificate shards, counted as source and never as claims. Navigation receives no proof authority: probe verdicts come from the pinned Lean process and cannot be authored by the agent, and a claim must cite an accepted probe that replay reruns from stored bytes.
- Explains
- the agent-navigation architecture: layered corpus projections, bounded intent routing, kernel-authored session receipts, focused builds, and exact dependency-index cache receipts.
- Not authority for
- proof validity, optimal reasoning, external mathematical novelty, or demonstrated transfer to another formalisation project.
Open the PDF · Read the LaTeX source · plectis-lean-erdos249-257
The evidence boundary
What may a stranger conclude from evidence whose author chose both what to publish and what counts as a pass?
Plectis: What a Stranger Can Check
What may a stranger conclude from public evidence when the author chose both what to publish and what counts as a pass?
The author publishes selected code, fixed inputs, expected results, decision rules, and run records while the larger system stays private. What can a stranger conclude after rerunning them? A matching result shows repeatability for one stated public case. It does not establish where the code came from, whether the expected answer is correct, whether the published selection resembles the private whole, or whether the private system works reliably. The contribution is a method for making one selected disagreement local, not a score.
Open the PDF · Read the LaTeX source · plectis
Retired manuscripts
Superseded work is not deleted. Each of these remains in its home repository so an existing citation still resolves, and each is marked so no reader mistakes it for the current route.
Irrationality Theorems for Reciprocal Mersenne Sums, and an Explicit Denominator Bound for the Binary Totient Series
What is mathematically proved about Erdős #249 and #257, and what exactly remains open?
The combined mathematical exposition for Erdős #249 and #257, superseded by the problem-specific notes and kept for provenance.
Retired: superseded by the problem-specific papers above, and kept here so an existing citation still resolves.
- Explains
- retired combined mathematical exposition preserved for provenance; its problem-specific successors are the active reader routes.
- Not authority for
- proof validity, which belongs to Lean source checked by the pinned kernel, and public claim status, which belongs to docs/claims.json.
- Where to start
- spines, architecture, unresolved (the paper's own reading route)
Open the PDF on GitHub · Read the LaTeX source · plectis-lean-erdos249-257