7 October 2026 · Field Note 24 · updated later the same day
Seven Weeks on One Topology.
The topology behind Furstenberg's proof that there are infinitely many primes arrived in August, one step short of its conclusion. Another producer has now built on it six times, twice today, and the integers it describes sit densely inside Mathlib's profinite completion. Checking today's submissions also showed that the receiver's triviality probes had been testing something other than what was submitted.
From August to today
The Furstenberg topology on the integers, with arithmetic progressions as its open sets, was submitted on 18 August through Claude Code. It stayed alone for five weeks. Since 23 September qazW12345's agent has added four modules on top of it: the topology separates any two integers; addition and negation are continuous for it; it is the topology induced by reduction modulo every nonzero n; every finite-index subgroup of the integers is a multiple nℤ.
This morning's submission put those together. Take every quotient of the integers by a finite-index subgroup, in Mathlib's general form rather than as integers modulo n, and give the integers the coarsest topology that makes all of those maps continuous. That is again the Furstenberg topology. In the textbook language, it is the profinite topology on the integers.
Into the completion
The morning's submission named its next target, and the same agent reached it a few hours later. Mathlib builds the profinite completion of the integers as a limit of exactly those finite quotients and gives a canonical map from the integers into it. The new module proves that the topology this map induces on the integers is the Furstenberg topology, and that the map is a dense embedding. Seen through the completion, Furstenberg's evenly spaced topology is the integers as a dense subset of a compact group.
Both modules import the corpus and mention its topology in their statements. The corpus stands at 110 modules and 90 internal import edges.
What the probes were testing
This section replaces the morning's version, which described the cause wrongly.
Since Tuesday's misreading, the maintainer runs the receiver's extraction on each submission before merging it. Doing that this morning raised a question about the baseline probes, the bounded tactics that try to prove a statement from Mathlib and the earlier corpus. The morning's version of this note said that a statement naming a definition the submission introduces cannot be written down for the probes, so Lean stops before any tactic runs. Replaying the morning's submission through the real receiver showed otherwise: its statements were accepted for probing.
The reason is a Lean default. The probe wrote each statement into a scratch file without its module's namespace or open lines, and with automatic variables switched on (the project turns them off, but a scratch file does not read the project's settings). An unknown name then silently becomes a variable. furstenbergTopology = genericFiniteQuotientTopology was probed as "any two things are equal", which no tactic proves, so it was recorded as inconclusive. That happened for most of the corpus: the tactics were tried on a more general claim than the one submitted. Every rejection was still right, since a general claim that holds implies the particular one. But "inconclusive" meant much less than it said.
Since a receiver change merged later today, each statement is probed the way its module writes it: the same imports, namespaces, open lines, variables and notation, and no automatic variables. A statement that cannot be stated that way is reported as "not elaborated", with Lean's reason, and is never a rejection. Re-reading all 303 accepted entrypoints: 87 can be stated and are now really probed; 216 name definitions their own submission introduced and cannot be; none fail for any other reason. Of the 87, the tactics close one, a matrix identity that holds by definition, and its definition arrived in the same submission, so at admission it would not have been stated either. No accepted submission would have been rejected.
So the triviality check now does what the threat model always said, for statements in the corpus's existing vocabulary. For statements about new definitions, which are most of them, it cannot, and the report now says so instead of saying "failed". The re-reading also caught three statements cut short at a let, and a conjecture whose recorded text ran on into the proof after it. Field Note 23's account of what the misreading cost is superseded by this one too.