P05 / LEVEL 11A cover that works for every n
Picture a rule like this: numbers that leave a remainder of 2 when divided by 7. A covering system is a set of these rules that, together, catch every number in a range. P05 builds a special kind, called an IRDCS, for the numbers 1 to n, for every n of 17 or more. The divisor in each rule is called its modulus, and here the smallest one is always at least 3. It uses a method called lane lifting, plus 351 finite certificates (computer-checkable records for specific cases). Lean, a program that checks every step of a proof, has checked the main theorem and the certificates. After the package was frozen, a stronger version followed: smallest modulus at least 4 for every n ≥ 17, also checked in Lean. Status: ready for expert review, not peer reviewed.
PS-L055 / LEVEL 11The smallest modulus can be as big as you like
Theorem M answers the second part of problem (1) from Myerson, Poon and Simpson. A human still needs to review it. Take any t of 5 or more that isn't divisible by 2 or 3 (“coprime to 6”). Then there's an explicit IRDCS of the numbers 1 to 45t. Its moduli run exactly from 12t−h to 31t+h, where h=(t−1)/2. So the smallest modulus grows without limit as t grows. It survived several independent checkers and a review of the write-up that tried hard to break it.
PS-L025 / LEVEL 11How a four-worker bucket brigade behaves
A bucket brigade is a way to share work along a line. Each worker carries a job forward. When the last worker finishes, each worker walks back and takes over the job of the person behind them. The first worker starts a new job. Here the four workers stand strictly fastest to slowest. A candidate theorem sorts every possible run. Each one either settles into the usual repeating pattern (the standard 4-cycle) or lands on one of exactly four unusual repeating patterns. A separate “blind” rebuild, made without seeing the original proof, reached the same theorem. It's ready for expert review, with clear notes on its limits and on tie cases.
PS-L071 / LEVEL 7All 20 Kuramoto steady states can be real
The Kuramoto model describes things that fall into sync, like fireflies flashing together. Here there are four of them, each linked to all the others. That's what K4 means here (nothing to do with Kryptos). If you also count solutions that use imaginary numbers, there can be up to 20 steady states. Can all 20 be real ones? This exactly checked example says yes. Every link pulls the four together (positive couplings), and each one has its own small, nonzero natural speed. Separate tools agree: Singular, PARI, msolve, Sturm and Krawczyk checks. A family of whole-number examples turned up too. It seems to answer the Baillieul–Byrnes question about real solutions for n=4. I still need to check the published papers, and a human expert still needs to review it.
PS-L075 / LEVEL 7Two open disc-packing cases knocked down
Imagine packing coins of three sizes on a table as tightly as you can. In a triangulated packing, every gap is boxed in by three coins that all touch each other. In Connelly's open cases 78 and 123, other packings (called binary-flow packings) beat every triangulated one. Exact algebra checks show it. The result survived an attempt to redo it and break it, plus an independent check. It's still AI-only evidence until a human expert checks the argument and how it fits the published work.
PS-L062 / LEVEL 7A counterexample in group testing (N=7)
Group testing saves tests by mixing samples and testing the mix. If the mix is clean, everyone in it is clear. Malinovsky's Conjecture 2 is a guess about the best testing plans. Read literally, with the starting order fixed, it fails. One exact case with N=7 has a nested plan that beats every GPTA order. A whole family of failures, given by a formula (a polynomial), was worked out and checked independently. A second reading of the conjecture, called adaptive pairing, is not ruled out. So which reading you use is part of the result.
HOW FAR ALONG IS IT?“New” isn't a yes-or-no thing.
Each claim has to pass a series of separate checks. Is the problem really open? Can we redo the known results? Is there a new signal? Does it survive a team trying to break it (a red team)? Can someone rebuild it independently? Is the reason it works clear? Does it answer the question exactly as stated? Has anyone done it before (a prior-art check)? Does it rerun cleanly? Is there a finished write-up? Is it ready to hand to an expert? Level 11 doesn't mean it's right, or that it's new. It means the AI-built evidence is solid enough to give to a specialist.
WHY P05 MATTERSThe best result builds an answer, not just a computer check.
The finite certificates aren't the theorem on their own. They're the first steps of an induction. That's a proof that works like dominoes: show the first ones fall, then show each one knocks over the next. Lane lifting keeps the modulus families apart by how many times 3 divides each modulus (its 3-adic structure). That turns a checked, limited range into a construction for every n ≥ 17. Finite checks inside a complete proof: that's the pattern the project is trying to repeat elsewhere.
BIG-PAYOFF SEARCHFinding a counterexample can be faster than proving a rule.
The Kuramoto, disc-packing and group-testing results all use the same lopsided fact. Finding an example might take a huge search, but checking it can be quick and exact. That suits coding agents really well. The search can be as wide as it needs to be, while the test for accepting an answer stays exact and repeatable.