PlectisThis repository studies eight Erdős problem programmes through short papers, longer research records, Lean proofs of selected statements, finite computations, and accounts of approaches that stopped. Plectis keeps the work open to further insight. The website brings the collection together; you do not need Lean to read it.
Start with the #257
paper: its checked finite-prime weighted criterion proves
irrationality for some infinite supports with divergent reciprocal sum,
while arbitrary infinite support remains open. Then read #1049:
irrationality holds in the stated region, including powers of
Using the degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement; the separate total-variation bound is also checked. The other seven targets remain open. Independent human review of correspondence with the 1958 wording has not been recorded. Comparator checks only selected exact statements, axioms and kernel acceptance; it does not assess novelty or historical correspondence.
Two ways to begin
You can follow one question or read across the corpus. The reading edition gives a short research instruction and the opening of each short paper in one file. For #257, follow the weighted theorem, its averaging proof, the long record and Lean source. Then try the weighted-support examples: change the base, or build a host with three minimal prime witnesses. A failed sufficient test proves nothing about rationality. The dyadic shift exercise tests another change of hypothesis.
Work through an argument
Try a small example before reading the proof. Note where your approach gets stuck, then find the step that overcomes that difficulty. Reconstruct it with the paper closed, or change a hypothesis and see what breaks.
If you use an agent, you can ask: “Help me work through this theorem. Give me one hint at a time and wait for my attempt before revealing more.” Name the paper, statement and your background. You choose the amount of help. The weighted-support exercise offers a place to start.
What is here
Each problem paper states the question, results and main arguments. The longer record keeps technical detail, failed routes, experiments and surviving obligations. The catalogue also includes system papers on proof boundaries, contribution and credit.
The results guide states the strongest checked result for each problem next to what still blocks its endpoint. Prior work records earlier arguments and attribution. Scope states the project’s limits; the architecture guide explains its machinery.
What formalisation adds
Lean checks a precise statement against a precise proof, exposing assumptions, quantifiers and dependencies. It does not establish novelty or importance, or turn a conditional result into an unconditional one. Each paper distinguishes ordinary mathematical arguments, formalised results and remaining gaps. Follow a statement’s source link and verification record to see what has been checked; a build alone does not establish that every argument in a paper has been formalised.
The eight problems in brief
Open a short paper below, or use the results guide for its arguments, formalisation and remaining questions.
Problem 68. Is the series sum_{n >= 2} 1/(n! - 1) irrational? Work on this paper.
Problem 243. Under a rapid-growth hypothesis on an integer sequence, does rationality of its reciprocal sum force the sequence to satisfy the Sylvester recurrence eventually? Work on this paper.
Problem 249. Is the binary Lambert series sum phi(n)/2^n irrational? Work on this paper.
Problem 251. Is the dyadic series of consecutive primes irrational? Equivalently, is the corresponding consecutive-prime-gap dyadic series irrational? Work on this paper.
Problem 257. Is the sum of 1/(2^n-1) over every infinite set of positive exponents irrational? Work on this paper.
Problem 269. For a finite set of at least two primes, is the sum of reciprocals of the running least common multiples of the smooth numbers irrational? This library treats the three-prime case. Work on this paper.
Problem 1041. Must two roots of a monic polynomial in the open unit disc be joined by a sub-two-length curve inside its unit lemniscate? Ani’s degree-seven example refutes the exact Formal Conjectures statement; correspondence with the 1958 wording awaits human review. Work on this paper.
Problem 1049. For which rational bases is the corresponding series irrational? The first resistant explicit base is three halves. Work on this paper.
The cross-problem paper, Reading Eight Erdős Problems Together joins the capacity criterion, Lambert subsums across bases, method limits, exact computations and unsuccessful approaches in one account. This is a central use of the collection: read the papers and Lean corpus together, find constructions or obstructions that survive in a more general setting, and develop the mathematics they suggest. The synthesis guide gives ways to begin.
How to read the evidence
The verification concordance at the end of each problem paper links its statements to Lean proofs and recorded Comparator checks. A dagger identifies a proof that assumes a named input; pending and partial support are labelled explicitly. These links appear in one place, leaving the mathematical argument uninterrupted.
Comparator compares selected statements with independently declared formal interfaces under fixed assumptions. It is not peer review and does not establish novelty. The Palomar guide distinguishes local packaging from recorded service submission or acceptance.
This is a self-contained public record, not an entrypoint into any private development system. A finite computation covers its tested range; file and declaration counts do not measure mathematical importance.
Reviewing one result
Pick a statement in a short paper, read its assumptions and the step that does the work, then follow the companion paper. Missing motivation, compressed hard steps and unclear attribution are useful feedback: a checked proof still needs an explanation others can understand and reuse.
Contributing
AI tools did much of the research, code, and drafting under my direction. I am responsible for the claims, the sources, and the release. Nothing here has had independent mathematical review.
Corrections, explanations, counterexamples and earlier references are welcome. The contributor guide explains how to return them with evidence and credit intact. If this work helps you solve a problem, the solution and credit are yours.
An insight is welcome before it has a formal proof. Will can work with you to develop the argument and formalise it, with the originating insight credited separately from subsequent exposition and proof work. Clearer understanding, reusable methods and new questions across the corpus also count as contributions; they need not close an original problem.