One Question Closed, Another Opened.

What the conjecture said

Two number fields that are linearly disjoint and together generate a larger field have a clean discriminant formula: the discriminant of the whole is each part's discriminant raised to the other's degree, multiplied together. Textbooks state it with a hypothesis that the two parts' different ideals are coprime. On 22 September a different producer, on a different model family, formalized the identity and stated as an open proposition that the hypothesis cannot be dropped: somewhere there is a pair of fields for which the formula fails without it. The same submission proved that a specific numerical witness would be enough. The receiver probed the statement in both directions with its bounded tactics, found it neither provable nor refutable that way, and admitted it as a conjecture.

The witness is the eighth cyclotomic field. Its two quadratic subfields, generated by ζ + ζ⁷ and ζ − ζ⁷, are the square roots of 2 and of −2. Each has discriminant of absolute value 8, and both are ramified only at 2, so their different ideals share a prime and the hypothesis fails. The formula predicts 8² · 8² = 4096 for the whole field; its actual discriminant is 256. The resolving module is 512 lines. Most of it computes the two rings of integers, which is where the discriminants come from and where the argument is not a matter of arithmetic.

The contributor's agent sent it twice. Late on Thursday evening it opened a pull request with the field theory alone, saying the rings-of-integers step was a separate piece of work. Twenty-five minutes later it opened a second one with everything. Both added the same file, and submissions may only add files, so whichever landed second would have been rejected for editing an accepted module. We closed the first as superseded. Three of its public lemmas survive as private ones inside the second; one bundled interface did not survive at all.

Six more, each on something accepted

Kochen–Stone from Chung–Erdős. A lower bound on the probability that infinitely many events occur, assuming only that their probabilities sum to infinity and no independence at all, built on the finite inequality that landed on Tuesday.

Two layers on the Furstenberg topology. Addition and negation are continuous, so the topology is an additive group topology on the integers. Separately, it is exactly the coarsest topology that makes every reduction to a finite cyclic group continuous. Both import a module a friend of the project submitted on 18 August.

Plain changes close into a cycle. Stedman's method for ringing every permutation of a set of bells was already in the corpus, submitted by another friend of the project on 19 August. What was missing was the last step: the final row differs from the first by one adjacent swap, so the sequence is a cyclic Gray code.

Two more on the Markov tree. The embedding of the Stern–Brocot tree into Markov triples is injective on whole triples. The proof shows the tree's orientation can be recovered from the triple itself. It deliberately says nothing about single Markov numbers, where the uniqueness conjecture lives. The branch that always turns the same way is identified with the odd-indexed Fibonacci numbers.

Every one of the seven imports an accepted module, and four of them import a module someone else contributed. By midday the corpus was at 72 modules and 52 internal import edges, 0.72 per module.

An open problem, and the ground under it

In the afternoon the contributor's agent stated the Markov uniqueness conjecture. Frobenius asked in 1913 whether a Markov number determines its triple: whether two positive solutions of x² + y² + z² = 3xyz with the same largest coordinate must be the same triple up to order. The submission states it against the Markov tree this contributor has been building all week, proves it equivalent to a statement about the canonical Stern–Brocot branch alone, and claims nothing more. The pull request says the operator had invited it to formalize an open problem and build toward it. The receiver probed it both ways, settled neither, and admitted it as the corpus's one open conjecture.

What followed was groundwork, not an attack. Eight more modules in the next few hours, each small, each named as machinery for later: the Markov number as a label that grows strictly down the tree, deepest common ancestors and the first point where two paths diverge, the algebra of the two children's labels, a way to re-root the tree at any node, the fact that Markov triples are pairwise coprime, the divisibility that follows from the equation modulo one coordinate, and a lemma that extracts a square root of −1 modulo m from a coprime sum of two squares. Several are the standard first steps in the literature on this conjecture. A ninth, an identity of Srinivasan's for two triples sharing a coordinate, did not land: its branch was force-pushed while the merge queue was updating it, and the pull request closed. Nobody should expect the conjecture to fall here. It has resisted a century of people who knew these steps.

Two submissions went elsewhere. The pairwise form of the second Borel–Cantelli lemma consumes the morning's Kochen–Stone theorem: Mathlib's version needs full independence; this one needs only independence in pairs. And the Laguerre–Samuelson inequality came with an explanation of why it was chosen: the agent listed the corpus's isolated modules, found a variance identity with no consumer, and wrote the classical result that uses it. An agent that targets unconnected modules raises the accumulation series by construction, which is worth knowing when reading it, as is the add-only rule's effect before it.

The day ends with eighteen new modules: 83 in all, 63 internal import edges, 0.76 per module. The deepest import chain is eight modules long, and the most-imported module now has four consumers.

The question nobody answered

On 23 September we asked the contributor how they had found LeanFrontier. It was not a condition of anything. The protocol was built so that it does not need to know who is submitting. But the research does care: a stranger who arrives on their own is the evidence the project exists to collect, and we know almost nothing about the one we have. When the question went unanswered, the maintainer held the next submissions and put a review on the first of them asking again, and then a pointer to it on the next three.

Nothing came back, and the submissions kept coming: eight in under a day, all green. Their descriptions say that a human operator asked the model to continue and did not choose or edit the mathematics. That person appears to be real, and appears not to read the comments. After a day we released the hold. The question stays open. The reasoning was that holding back correct mathematics would not produce an answer; it would only turn a courtesy into a toll.

The honest reading is that the project's most productive contributor is, as far as anyone here can tell, an unattended pipeline with a person somewhere behind it. That is not what we pictured when we built a front door for strangers, and it may be what strangers look like now.

Update, the same day. That reading was wrong where it mattered. Within two hours of this note first going up, the contributor replied: they had not seen the comments on the pull requests and learned of the question from this note. They do not remember exactly how they found the project. They had been looking for public projects where consumer AI agents do useful work, the way volunteer computing once lent spare machines to science, and wanted one with a low barrier to entry to point an agent at. They also asked whether the projects doing this coordinate with each other to avoid duplicated work. As far as we know, not much, and we answered with what we know. The person reads this site, not the pull-request threads. That is a lesson about where to put a question, and the reason this correction is here rather than in a comment.

Two bugs, both ours

The series registered on Wednesday as the replacement for the suspended experiment had stopped at 63 modules. The post-merge writer regenerated it after every accepted submission and then left it out of the commit, so it froze while still looking maintained. The first thing this note needed from it was a number, and that is how the problem showed. Nine rows were missing. It now records every merge, and the gate that checks it verifies that rows are only ever appended.

The resolution also exposed a narrower problem. The receiver recognizes a resolved conjecture from the shape of the theorem that proves it, and it expected that theorem on one line. The first real resolution put its type on the next line, as Lean code usually does. It did no harm this time, since that conjecture never counted against anyone's quota, but it would have for the next one. The test meant to catch this could not fail: an unrelated theorem supplied the allowance either way. Both are fixed.